# HG changeset patch
# User wenzelm
# Date 1354826780 -3600
# Node ID c28753665b8e46c38e1760de963e6046c2aa4777
# Parent  366c4a6025007f927ca64d78282467682de6deca
documentation for isabelle build_dialog and its implicit use in isabelle jedit;

diff -r 366c4a602500 -r c28753665b8e NEWS
--- 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.
diff -r 366c4a602500 -r c28753665b8e src/Doc/System/Interfaces.thy
--- 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 *}
diff -r 366c4a602500 -r c28753665b8e src/Doc/System/Sessions.thy
--- 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