Re: [isabelle] splash?



On Wed, 21 Oct 2015, Rustom Mody wrote:

Starting as
$ Isabelle.run
always opens scratch.thy
Starting as
$ Isabelle.run -nosplash
opens blank

Is this the expected behavior?

Yes, because the command-line is non-empty and thus there is no default added.


Note that Isabelle.run is merely an auxiliary script to the main Isabelle application wrapper on Linux. You normally invoke it by double-clicking on the Desktop.

Command-line invocations are done with "isabelle jedit" and its various options. A short description is printed like this:

  Isabelle2015/bin/isabelle jedit -?

A long description is in the "jedit" manual, which is accessible in the Document panel, or on the command-line like this:

  Isabelle2015/bin/isabelle doc jedit


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.