[isabelle-dev] NEWS: isabelle jedit options

[Makarius]

On 06/06/18 16:19, Lawrence Paulson wrote:
> 
> 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.
> 

It could just mean that these examples don't need an auxiliary image.

Take the first example from NEWS:

  isabelle jedit -R HOL-Number_Theory

It produces an image
"HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also
the title line of Isabelle/jEdit.

It also puts you into the ROOT entry for HOL-Number_Theory, so you can
directly explore its theories in the Prover IDE.


	Makarius