# HG changeset patch # User wenzelm # Date 1402339260 -7200 # Node ID 00f2c8d1aa0b9580340edb8ae7eae923f1fbc3e5 # Parent 3ca8216f4a96b2f27bb129a2d02ed427d1981148 more on command-line invocation -- moved material from system manual; diff -r 3ca8216f4a96 -r 00f2c8d1aa0b src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Mon Jun 09 19:55:58 2014 +0200 +++ b/src/Doc/JEdit/JEdit.thy Mon Jun 09 20:41:00 2014 +0200 @@ -217,6 +217,61 @@ "$ISABELLE_HOME_USER/jedit/keymaps"}). *} +section {* Command-line invocation *} + +text {* + Isabelle/jEdit is normally invoked as standalone application, with + platform-specific executable wrappers for Linux, Windows, Mac OS X. + Nonetheless it is occasionally useful to invoke the Prover IDE on the + command-line, with some extra options and environment settings as explained + below. The command-line usage of @{tool_def jedit} is as follows: +\begin{ttbox} + Usage: isabelle jedit [OPTIONS] [FILES ...] + + Options are: + -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) + -b build only + -d DIR include session directory + -f fresh build + -j OPTION add jEdit runtime option (default JEDIT_OPTIONS) + -l NAME logic image name (default ISABELLE_LOGIC) + -m MODE add print mode for output + -n no build of session image on startup + -s system build mode for session image + + Start jEdit with Isabelle plugin setup and open theory FILES + (default "\$USER_HOME/Scratch.thy"). +\end{ttbox} + + The @{verbatim "-l"} option specifies the session name of the logic + image to be used for proof processing. Additional session root + directories may be included via option @{verbatim "-d"} to augment + that name space of @{tool build} \cite{isabelle-sys}. + + By default, the specified image is checked and built on demand. The + @{verbatim "-s"} option determines where to store the result session image + of @{tool build}. The @{verbatim "-n"} option bypasses the implicit build + process for the selected session image. + + The @{verbatim "-m"} option specifies additional print modes for the + prover process. Note that the system option @{system_option + jedit_print_mode} allows to do the same persistently (e.g.\ via the + Plugin Options dialog of Isabelle/jEdit), without requiring + command-line invocation. + + The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass + additional low-level options to the JVM or jEdit, respectively. The + defaults are provided by the Isabelle settings environment + \cite{isabelle-sys}. + + The @{verbatim "-b"} and @{verbatim "-f"} options control the self-build + mechanism of Isabelle/jEdit. This is only relevant for building from + sources, which also requires an auxiliary @{verbatim jedit_build} component + from @{url "http://isabelle.in.tum.de/components"}. Note that official + Isabelle releases already include a pre-built version of Isabelle/jEdit. +*} + + chapter {* Augmented jEdit functionality *} section {* Look-and-feel *} @@ -587,13 +642,12 @@ \emph{isabelle} and treated specifically. \medskip Isabelle theory files are automatically added to the formal - document model of Isabelle/Scala, which maintains a family of - versions of all sources for the prover. The \emph{Theories} panel - provides an overview of the status of continuous checking of theory - sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes - are identified by full path names; this allows to work with multiple - (disjoint) Isabelle sessions simultaneously within the same editor - session. + document model of Isabelle/Scala, which maintains a family of versions of + all sources for the prover. The \emph{Theories} panel provides an overview + of the status of continuous checking of theory sources. Unlike batch + sessions of @{tool build} \cite{isabelle-sys}, theory nodes are identified + by full path names; this allows to work with multiple (disjoint) Isabelle + sessions simultaneously within the same editor session. Certain events to open or update buffers with theory files cause Isabelle/jEdit to resolve dependencies of \emph{theory imports}. The system diff -r 3ca8216f4a96 -r 00f2c8d1aa0b src/Doc/System/Interfaces.thy --- a/src/Doc/System/Interfaces.thy Mon Jun 09 19:55:58 2014 +0200 +++ b/src/Doc/System/Interfaces.thy Mon Jun 09 20:41:00 2014 +0200 @@ -4,61 +4,11 @@ chapter {* User interfaces *} -section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *} - -text {* The @{tool_def jedit} tool invokes a version of - jEdit\footnote{@{url "http://www.jedit.org/"}} that has been augmented - with some plugins to provide a fully-featured Prover IDE: -\begin{ttbox} Usage: isabelle jedit [OPTIONS] - [FILES ...] - - Options are: - -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) - -b build only - -d DIR include session directory - -f fresh build - -j OPTION add jEdit runtime option (default JEDIT_OPTIONS) - -l NAME logic image name (default ISABELLE_LOGIC) - -m MODE add print mode for output - -n no build of session image on startup - -s system build mode for session image - - Start jEdit with Isabelle plugin setup and open theory FILES - (default "\$USER_HOME/Scratch.thy"). -\end{ttbox} - - The @{verbatim "-l"} option specifies the session name of the logic - image to be used for proof processing. Additional session root - directories may be included via option @{verbatim "-d"} to augment - that name space (see also \secref{sec:tool-build}). - - By default, the specified image is checked and built on demand. The - @{verbatim "-s"} option determines where to store the result session - image (see also \secref{sec:tool-build}). The @{verbatim "-n"} - option bypasses the implicit build process for the selected session - image. - - The @{verbatim "-m"} option specifies additional print modes for the - prover process. Note that the system option @{system_option - jedit_print_mode} allows to do the same persistently (e.g.\ via the - Plugin Options dialog of Isabelle/jEdit), without requiring - command-line invocation. - - The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass - additional low-level options to the JVM or jEdit, respectively. The - defaults are provided by the Isabelle settings environment - (\secref{sec:settings}). - - The @{verbatim "-b"} and @{verbatim "-f"} options control the - self-build mechanism of Isabelle/jEdit. This is only relevant for - building from sources, which also requires an auxiliary @{verbatim - jedit_build} - component.\footnote{@{url "http://isabelle.in.tum.de/components"}} Note - that official Isabelle releases already include a version of - Isabelle/jEdit that is built properly. +text {* + The default user-interface and Prover IDE is Isabelle/jEdit, which is + described in a separate manual \cite{isabelle-jedit}. *} - section {* Proof General / Emacs *} text {* The @{tool_def emacs} tool invokes a version of Emacs and diff -r 3ca8216f4a96 -r 00f2c8d1aa0b src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy Mon Jun 09 19:55:58 2014 +0200 +++ b/src/Doc/System/Scala.thy Mon Jun 09 20:41:00 2014 +0200 @@ -8,7 +8,7 @@ environments for Isabelle tool implementations. There are some basic command-line tools to work with the underlying Java Virtual Machine, the Scala toplevel and compiler. Note that Isabelle/jEdit -(\secref{sec:tool-tty}) provides a Scala Console for interactive +\cite{isabelle-jedit} provides a Scala Console for interactive experimentation within the running application. *} @@ -66,7 +66,7 @@ add-on components can register themselves in a modular manner, see also \secref{sec:components}. - Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for + Note that jEdit \cite{isabelle-jedit} has its own mechanisms for adding plugin components, which needs special attention since it overrides the standard Java class loader. *} diff -r 3ca8216f4a96 -r 00f2c8d1aa0b src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Mon Jun 09 19:55:58 2014 +0200 +++ b/src/Doc/System/Sessions.thy Mon Jun 09 20:41:00 2014 +0200 @@ -44,7 +44,7 @@ organize browser info (\secref{sec:info}), but have no formal meaning. The default chapter is ``@{text "Unsorted"}''. - Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing + Isabelle/jEdit \cite{isabelle-jedit} includes a simple editing mode @{verbatim "isabelle-root"} for session ROOT files, which is enabled by default for any file of that name. @@ -161,7 +161,7 @@ section {* System build options \label{sec:system-options} *} text {* See @{file "~~/etc/options"} for the main defaults provided by - the Isabelle distribution. Isabelle/jEdit (\secref{sec:tool-jedit}) + the Isabelle distribution. Isabelle/jEdit \cite{isabelle-jedit} includes a simple editing mode @{verbatim "isabelle-options"} for this file-format. diff -r 3ca8216f4a96 -r 00f2c8d1aa0b src/Doc/manual.bib --- a/src/Doc/manual.bib Mon Jun 09 19:55:58 2014 +0200 +++ b/src/Doc/manual.bib Mon Jun 09 20:41:00 2014 +0200 @@ -1784,6 +1784,12 @@ institution = {TU Munich}, note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}} +@manual{isabelle-jedit, + author = {Makarius Wenzel}, + title = {{Isabelle/jEdit}}, + institution = {TU Munich}, + note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}} + @manual{isabelle-isar-ref, author = {Makarius Wenzel}, title = {The {Isabelle/Isar} Reference Manual},