Re: [isabelle-dev] Diagnostic commands in jedit?

2011-09-30 Thread Florian Haftmann
 Things like code generation might be of the form of associating document
 content that is generated by functional evaluation over the semantics of
 the formal source text.  Think of it as part of browser_info, not the
 src tree.  Part of the question is who or what is the target of
 generated sources.  One might consider funny ways to refer to
 resources of a theory node, similar to the way 'uses' are located now
 within the file-system wrt. the master directory, but without an actual
 physical directory.

I was actually thinking in a similar direction.  So a first step would
be to come up with an idea how to integrate document preparation into
the IDE-style user interaction of Isabelle/jedit without the current
low-level tinkering we are doing at the moment (batch sessions,
makefiles, arcane ROOT files etc.)

Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Isabelle_11-Sep-2011

2011-09-30 Thread Bertram Felgenhauer
Dear Makarius and René,

 However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a 
 problem for Mac OS Lion users:
 Many special characters like == \in, = are not displayed correctly which 
 makes working inconvenient. Under
 
 http://cl-informatik.uibk.ac.at/~thiemann/emacs.html

I believe I know this bug. It's an emacs problem, and should be fixed in
emacs 23.4 once it becomes available. That said I don't know of any elisp
code other than ProofGeneral that tickles this bug. As far as Isabell/PG
are concerned, it's not a new problem -- it also affects Isabelle2011. See

  http://debbugs.gnu.org/cgi/bugreport.cgi?bug=8703

(Note that I encountered this problem with Linux -- I hope that the MacOS
version uses the same code, but I have not tested this theory.)

Best regards,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Isabelle_11-Sep-2011

2011-09-30 Thread Makarius

On Fri, 30 Sep 2011, Bertram Felgenhauer wrote:


Dear Makarius and René,


However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a 
problem for Mac OS Lion users:
Many special characters like == \in, = are not displayed correctly which 
makes working inconvenient. Under

http://cl-informatik.uibk.ac.at/~thiemann/emacs.html


I believe I know this bug. It's an emacs problem, and should be fixed in 
emacs 23.4 once it becomes available. That said I don't know of any 
elisp code other than ProofGeneral that tickles this bug. As far as 
Isabell/PG are concerned, it's not a new problem -- it also affects 
Isabelle2011. See


 http://debbugs.gnu.org/cgi/bugreport.cgi?bug=8703

(Note that I encountered this problem with Linux -- I hope that the 
MacOS version uses the same code, but I have not tested this theory.)


What is odd about it: with the same Emacs-23.2.1 on Mac OS X the problem 
only occurs on Lion, not Snow Leopard (which I have started to re-install 
today on my desktop system).


Since Emacs-23.2.1 has only a *few* such drop-outs on Lion, but Emacs-23.3 
has *many*, I have switched back to the older version in the app bundle on 
http://isabelle.in.tum.de/website-Isabelle2011-1-RC1/



Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev