--- a/NEWS Thu Dec 06 21:16:46 2012 +0100
+++ b/NEWS Thu Dec 06 21:46:20 2012 +0100
@@ -91,6 +91,11 @@
adjust the main text area font size, and its derivatives for output,
tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS.
+* Implicit check and build dialog of the specified logic session
+image. For example, HOL, HOLCF, HOL-Nominal can be produced on
+demand, without bundling big platform-dependent heap images in the
+Isabelle distribution.
+
* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
from Oracle provide better multi-platform experience. This version is
now bundled exclusively with Isabelle.
--- a/src/Doc/System/Interfaces.thy Thu Dec 06 21:16:46 2012 +0100
+++ b/src/Doc/System/Interfaces.thy Thu Dec 06 21:46:20 2012 +0100
@@ -20,6 +20,8 @@
-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 dialog for session image on startup
+ -s system build mode for session image
Start jEdit with Isabelle plugin setup and opens theory FILES
(default Scratch.thy).
@@ -30,6 +32,11 @@
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, see
+ also @{tool build_dialog}. The @{verbatim "-s"} determines where to
+ store the result session image (see also \secref{sec:tool-build}).
+ The @{verbatim "-n"} option bypasses the session build dialog.
+
The @{verbatim "-m"} option specifies additional print modes.
The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
@@ -43,7 +50,8 @@
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. *}
+ Isabelle/jEdit that is built properly.
+*}
section {* Proof General / Emacs *}
--- a/src/Doc/System/Sessions.thy Thu Dec 06 21:16:46 2012 +0100
+++ b/src/Doc/System/Sessions.thy Thu Dec 06 21:46:20 2012 +0100
@@ -334,4 +334,29 @@
\end{ttbox}
*}
+
+section {* Build dialog *}
+
+text {* The @{tool_def build_dialog} provides a simple GUI wrapper to
+ the tool Isabelle @{tool build} tool. This enables user interfaces
+ like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made
+ logic image on startup. Its command-line usage is:
+\begin{ttbox}
+Usage: isabelle build_dialog [OPTIONS] LOGIC
+
+ Options are:
+ -L OPTION default logic via system option
+ -d DIR include session directory
+ -s system build mode: produce output in ISABELLE_HOME
+
+ Build Isabelle session image LOGIC via GUI dialog.
+\end{ttbox}
+
+ \medskip Option @{verbatim "-L"} specifies a system option name as
+ fall-back, if the specified @{text "LOGIC"} name is empty.
+
+ \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
+ meaning as for the command-line @{tool build} tool itself.
+*}
+
end