--- 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
--- 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
--- 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. *}
--- 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.
--- 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},