[isabelle-dev] NEWS: isabelle jedit options

Lawrence Paulson lp15 at cam.ac.uk
Wed Jun 6 16:19:54 CEST 2018


> On 6 Jun 2018, at 12:43, Makarius <makarius at sketis.net> wrote:
> 
> On 06/06/18 12:45, Lawrence Paulson wrote:
>> I saw them of course, but what do they do?
> 
> These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
> have simplified and clarified the situation, updated NEWS and
> documentation in the "jedit" manual.
> 
> Right now the main question is if this is sufficient for the release,
> and the documentation clear.

Having tinkered with these things, read the NEWS entry and read the relevant section of the manual, I am still completely in the dark.

According to the NEWS entry, option -R builds an auxiliary logic image. I tried this with a couple of examples and no images were built. According to the manual, this option opens the ROOT entry. It does seem to do that, though I'm not sure why this facility is needed.

Surely it wouldn't be difficult to add a few lines of text, describing the sort of situation in which this option is useful.

Larry


More information about the isabelle-dev mailing list