Re: [isabelle-dev] weird error message on startup

2017-12-06 Thread Makarius
On 06/12/17 15:48, Lawrence Paulson wrote: > I've just updated to a recent version (fa1173288322) and tried to run a > session by the following command: > > isabelle jedit -l HOL-Analysis CV.thy > > And then I get an alert box containing the appended text. Any idea what's > going wrong here?

Re: [isabelle-dev] NEWS: antiquoted cartouches

2017-12-06 Thread Makarius
On 05/12/17 17:18, Makarius wrote: > *** Prover IDE -- Isabelle/Scala/jEdit *** > > * Named control symbols (without special Unicode rendering) are shown as > bold-italic keyword. This is particularly useful for the short form of > antiquotations with control symbol: \<^name>\argument\. The >

Re: [isabelle-dev] weird error message on startup

2017-12-06 Thread Tobias Nipkow
I have modified HOL-Analysis but broke latex as a result. I have undone it again just now. No idea if this has anything to do with your problem. Tobias On 06/12/2017 15:48, Lawrence Paulson wrote: I've just updated to a recent version (fa1173288322) and tried to run a session by the

[isabelle-dev] weird error message on startup

2017-12-06 Thread Lawrence Paulson
I've just updated to a recent version (fa1173288322) and tried to run a session by the following command: isabelle jedit -l HOL-Analysis CV.thy And then I get an alert box containing the appended text. Any idea what's going wrong here? Larry Cannot load theory file

Re: [isabelle-dev] NEWS: document_tags

2017-12-06 Thread Tobias Nipkow
On 05/12/2017 17:21, Makarius wrote: *** Document preparation *** * System option "document_tags" specifies a default for otherwise untagged commands. This is occasionally useful to control the global visibility of commands via session options (e.g. in ROOT). * Document markup commands