Re: [isabelle-dev] print modes

2012-05-01 Thread Brian Huffman 
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
 is it really the case that currently the only way to obtain ASCII output
 using print modes is by specifying the empty string, like

 thm () conjE

 or did I miss anything? Since this print mode is occasionally useful, I
 suggest to provide a named variant, like 'plain', 'ASCII', or whatever.

+1

I would actually go a bit further, and get rid of xsymbol as a
special syntax mode.

It bothers me that if I want to define a constant with both ascii and
symbol notation, I have to use the ascii variant in the actual
definition, and then add the (far more commonly-used) symbol notation
later.

definition foo :: 'a = 'a = bool (infix ~~ 50) where ...
notation (xsymbol) foo (infix \approx 50)

I would rather write:

definition foo :: 'a = 'a = bool (infix \approx 50) where ...
notation (ascii) foo (infix ~~ 50)

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

[isabelle-dev] jEdit

2012-05-01 Thread Christian Sternagel 

Dear Makarius,

would it make sense to introduce some kind of read-only mode for 
theory files and then use this mode when jumping to a file that is 
already finished (instead of the Attempt to update loaded theory ... 
error message)?


Of course I don't know whether it is easily possible to distinguish 
between files that are already loaded as part of a heap image and files 
that are loaded by hand (which should not be loaded in read-only mode).


On a related note: the output of such loaded files is still interesting. 
Is there any way to make the output immediately available from the heap 
image, without actually loading the theory (in the end it was already 
loaded when creating the heap image, but I guess the output is a 
side-effect and not part of the resulting heap)?


cheers

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