documentation for isabelle build_dialog and its implicit use in isabelle jedit;
authorwenzelm
Thu Dec 06 21:46:20 2012 +0100 (2012-12-06)
changeset 50406c28753665b8e
parent 50405 366c4a602500
child 50407 ebc118cd232a
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
NEWS
src/Doc/System/Interfaces.thy
src/Doc/System/Sessions.thy
     1.1 --- a/NEWS	Thu Dec 06 21:16:46 2012 +0100
     1.2 +++ b/NEWS	Thu Dec 06 21:46:20 2012 +0100
     1.3 @@ -91,6 +91,11 @@
     1.4  adjust the main text area font size, and its derivatives for output,
     1.5  tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS.
     1.6  
     1.7 +* Implicit check and build dialog of the specified logic session
     1.8 +image.  For example, HOL, HOLCF, HOL-Nominal can be produced on
     1.9 +demand, without bundling big platform-dependent heap images in the
    1.10 +Isabelle distribution.
    1.11 +
    1.12  * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
    1.13  from Oracle provide better multi-platform experience.  This version is
    1.14  now bundled exclusively with Isabelle.
     2.1 --- a/src/Doc/System/Interfaces.thy	Thu Dec 06 21:16:46 2012 +0100
     2.2 +++ b/src/Doc/System/Interfaces.thy	Thu Dec 06 21:46:20 2012 +0100
     2.3 @@ -20,6 +20,8 @@
     2.4      -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
     2.5      -l NAME      logic image name (default ISABELLE_LOGIC)
     2.6      -m MODE      add print mode for output
     2.7 +    -n           no build dialog for session image on startup
     2.8 +    -s           system build mode for session image
     2.9  
    2.10  Start jEdit with Isabelle plugin setup and opens theory FILES
    2.11  (default Scratch.thy).
    2.12 @@ -30,6 +32,11 @@
    2.13    directories may be included via option @{verbatim "-d"} to augment
    2.14    that name space (see also \secref{sec:tool-build}).
    2.15  
    2.16 +  By default, the specified image is checked and built on demand, see
    2.17 +  also @{tool build_dialog}.  The @{verbatim "-s"} determines where to
    2.18 +  store the result session image (see also \secref{sec:tool-build}).
    2.19 +  The @{verbatim "-n"} option bypasses the session build dialog.
    2.20 +
    2.21    The @{verbatim "-m"} option specifies additional print modes.
    2.22  
    2.23    The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
    2.24 @@ -43,7 +50,8 @@
    2.25    jedit_build}
    2.26    component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
    2.27    that official Isabelle releases already include a version of
    2.28 -  Isabelle/jEdit that is built properly.  *}
    2.29 +  Isabelle/jEdit that is built properly.
    2.30 +*}
    2.31  
    2.32  
    2.33  section {* Proof General / Emacs *}
     3.1 --- a/src/Doc/System/Sessions.thy	Thu Dec 06 21:16:46 2012 +0100
     3.2 +++ b/src/Doc/System/Sessions.thy	Thu Dec 06 21:46:20 2012 +0100
     3.3 @@ -334,4 +334,29 @@
     3.4  \end{ttbox}
     3.5  *}
     3.6  
     3.7 +
     3.8 +section {* Build dialog *}
     3.9 +
    3.10 +text {* The @{tool_def build_dialog} provides a simple GUI wrapper to
    3.11 +  the tool Isabelle @{tool build} tool.  This enables user interfaces
    3.12 +  like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made
    3.13 +  logic image on startup.  Its command-line usage is:
    3.14 +\begin{ttbox}
    3.15 +Usage: isabelle build_dialog [OPTIONS] LOGIC
    3.16 +
    3.17 +  Options are:
    3.18 +    -L OPTION    default logic via system option
    3.19 +    -d DIR       include session directory
    3.20 +    -s           system build mode: produce output in ISABELLE_HOME
    3.21 +
    3.22 +  Build Isabelle session image LOGIC via GUI dialog.
    3.23 +\end{ttbox}
    3.24 +
    3.25 +  \medskip Option @{verbatim "-L"} specifies a system option name as
    3.26 +  fall-back, if the specified @{text "LOGIC"} name is empty.
    3.27 +
    3.28 +  \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
    3.29 +  meaning as for the command-line @{tool build} tool itself.
    3.30 +*}
    3.31 +
    3.32  end