src/Doc/System/Interfaces.thy
 author wenzelm Fri May 17 19:04:52 2013 +0200 (2013-05-17) changeset 52056 fc458f304f93 parent 51054 d6de6e81574d child 52062 4f91262e7f33 permissions -rw-r--r--
     1 theory Interfaces

     2 imports Base

     3 begin

     4

     5 chapter {* User interfaces *}

     6

     7 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}

     8

     9 text {* The @{tool_def jedit} tool invokes a version of

    10   jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented

    11   with some plugins to provide a fully-featured Prover IDE:

    12 \begin{ttbox} Usage: isabelle jedit [OPTIONS]

    13   [FILES ...]

    14

    15   Options are:

    16     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)

    17     -b           build only

    18     -d DIR       include session directory

    19     -f           fresh build

    20     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)

    21     -l NAME      logic image name (default ISABELLE_LOGIC)

    22     -m MODE      add print mode for output

    23     -n           no build dialog for session image on startup

    24     -s           system build mode for session image

    25

    26 Start jEdit with Isabelle plugin setup and open theory FILES

    27 (default "\\$USER_HOME/Scratch.thy").

    28 \end{ttbox}

    29

    30   The @{verbatim "-l"} option specifies the session name of the logic

    31   image to be used for proof processing.  Additional session root

    32   directories may be included via option @{verbatim "-d"} to augment

    33   that name space (see also \secref{sec:tool-build}).

    34

    35   By default, the specified image is checked and built on demand, see

    36   also @{tool build_dialog}.  The @{verbatim "-s"} determines where to

    37   store the result session image (see also \secref{sec:tool-build}).

    38   The @{verbatim "-n"} option bypasses the session build dialog.

    39

    40   The @{verbatim "-m"} option specifies additional print modes for the

    41   prover process.

    42

    43   The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass

    44   additional low-level options to the JVM or jEdit, respectively.  The

    45   defaults are provided by the Isabelle settings environment

    46   (\secref{sec:settings}).

    47

    48   The @{verbatim "-b"} and @{verbatim "-f"} options control the

    49   self-build mechanism of Isabelle/jEdit.  This is only relevant for

    50   building from sources, which also requires an auxiliary @{verbatim

    51   jedit_build}

    52   component.\footnote{\url{http://isabelle.in.tum.de/components}} Note

    53   that official Isabelle releases already include a version of

    54   Isabelle/jEdit that is built properly.

    55 *}

    56

    57

    58 section {* Proof General / Emacs *}

    59

    60 text {* The @{tool_def emacs} tool invokes a version of Emacs and

    61   Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the

    62   regular Isabelle settings environment (\secref{sec:settings}).  This

    63   is more convenient than starting Emacs separately, loading the Proof

    64   General LISP files, and then attempting to start Isabelle with

    65   dynamic @{setting PATH} lookup etc., although it might fail if a

    66   different version of Proof General is already part of the Emacs

    67   installation of the operating system.

    68

    69   The actual interface script is part of the Proof General

    70   distribution; its usage depends on the particular version.  There

    71   are some options available, such as @{verbatim "-l"} for passing the

    72   logic image to be used by default, or @{verbatim "-m"} to tune the

    73   standard print mode of the prover process.  The following Isabelle

    74   settings are particularly important for Proof General:

    75

    76   \begin{description}

    77

    78   \item[@{setting_def PROOFGENERAL_HOME}] points to the main

    79   installation directory of the Proof General distribution.  This is

    80   implicitly provided for versions of Proof General that are

    81   distributed as Isabelle component, see also \secref{sec:components};

    82   otherwise it needs to be configured manually.

    83

    84   \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to

    85   the command line of any invocation of the Proof General @{verbatim

    86   interface} script.  This allows to provide persistent default

    87   options for the invocation of \texttt{isabelle emacs}.

    88

    89   \end{description}

    90 *}

    91

    92

    93 section {* Plain TTY interaction \label{sec:tool-tty} *}

    94

    95 text {*

    96   The @{tool_def tty} tool runs the Isabelle process interactively

    97   within a plain terminal session:

    98 \begin{ttbox}

    99 Usage: isabelle tty [OPTIONS]

   100

   101   Options are:

   102     -l NAME      logic image name (default ISABELLE_LOGIC)

   103     -m MODE      add print mode for output

   104     -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)

   105

   106   Run Isabelle process with plain tty interaction and line editor.

   107 \end{ttbox}

   108

   109   The @{verbatim "-l"} option specifies the logic image.  The

   110   @{verbatim "-m"} option specifies additional print modes.  The

   111   @{verbatim "-p"} option specifies an alternative line editor (such

   112   as the @{executable_def rlwrap} wrapper for GNU readline); the

   113   fall-back is to use raw standard input.

   114

   115   Regular interaction works via the standard Isabelle/Isar toplevel

   116   loop.  The Isar command @{command exit} drops out into the

   117   bare-bones ML system, which is occasionally useful for debugging of

   118   the Isar infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim

   119   "();"} in ML will return to the Isar toplevel.  *}

   120

   121

   122

   123 section {* Theory graph browser \label{sec:browse} *}

   124

   125 text {* The Isabelle graph browser is a general tool for visualizing

   126   dependency graphs.  Certain nodes of the graph (i.e.\ theories) can

   127   be grouped together in directories'', whose contents may be

   128   hidden, thus enabling the user to collapse irrelevant portions of

   129   information.  The browser is written in Java, it can be used both as

   130   a stand-alone application and as an applet.  *}

   131

   132

   133 subsection {* Invoking the graph browser *}

   134

   135 text {* The stand-alone version of the graph browser is wrapped up as

   136   @{tool_def browser}:

   137 \begin{ttbox}

   138 Usage: isabelle browser [OPTIONS] [GRAPHFILE]

   139

   140   Options are:

   141     -b           Admin/build only

   142     -c           cleanup -- remove GRAPHFILE after use

   143     -o FILE      output to FILE (ps, eps, pdf)

   144 \end{ttbox}

   145   When no filename is specified, the browser automatically changes to

   146   the directory @{setting ISABELLE_BROWSER_INFO}.

   147

   148   \medskip The @{verbatim "-b"} option indicates that this is for

   149   administrative build only, i.e.\ no browser popup if no files are

   150   given.

   151

   152   The @{verbatim "-c"} option causes the input file to be removed

   153   after use.

   154

   155   The @{verbatim "-o"} option indicates batch-mode operation, with the

   156   output written to the indicated file; note that @{verbatim pdf}

   157   produces an @{verbatim eps} copy as well.

   158

   159   \medskip The applet version of the browser is part of the standard

   160   WWW theory presentation, see the link theory dependencies'' within

   161   each session index.

   162 *}

   163

   164

   165 subsection {* Using the graph browser *}

   166

   167 text {*

   168   The browser's main window, which is shown in

   169   \figref{fig:browserwindow}, consists of two sub-windows.  In the

   170   left sub-window, the directory tree is displayed. The graph itself

   171   is displayed in the right sub-window.

   172

   173   \begin{figure}[ht]

   174   \includegraphics[width=\textwidth]{browser_screenshot}

   175   \caption{\label{fig:browserwindow} Browser main window}

   176   \end{figure}

   177 *}

   178

   179

   180 subsubsection {* The directory tree window *}

   181

   182 text {*

   183   We describe the usage of the directory browser and the meaning of

   184   the different items in the browser window.

   185

   186   \begin{itemize}

   187

   188   \item A red arrow before a directory name indicates that the

   189   directory is currently folded'', i.e.~the nodes in this directory

   190   are collapsed to one single node. In the right sub-window, the names

   191   of nodes corresponding to folded directories are enclosed in square

   192   brackets and displayed in red color.

   193

   194   \item A green downward arrow before a directory name indicates that

   195   the directory is currently unfolded''. It can be folded by

   196   clicking on the directory name.  Clicking on the name for a second

   197   time unfolds the directory again.  Alternatively, a directory can

   198   also be unfolded by clicking on the corresponding node in the right

   199   sub-window.

   200

   201   \item Blue arrows stand before ordinary node names. When clicking on

   202   such a name (i.e.\ that of a theory), the graph display window

   203   focuses to the corresponding node. Double clicking invokes a text

   204   viewer window in which the contents of the theory file are

   205   displayed.

   206

   207   \end{itemize}

   208 *}

   209

   210

   211 subsubsection {* The graph display window *}

   212

   213 text {*

   214   When pointing on an ordinary node, an upward and a downward arrow is

   215   shown.  Initially, both of these arrows are green. Clicking on the

   216   upward or downward arrow collapses all predecessor or successor

   217   nodes, respectively. The arrow's color then changes to red,

   218   indicating that the predecessor or successor nodes are currently

   219   collapsed. The node corresponding to the collapsed nodes has the

   220   name @{verbatim "[....]"}''. To uncollapse the nodes again, simply

   221   click on the red arrow or on the node with the name @{verbatim

   222   "[....]"}''. Similar to the directory browser, the contents of

   223   theory files can be displayed by double clicking on the

   224   corresponding node.

   225 *}

   226

   227

   228 subsubsection {* The File'' menu *}

   229

   230 text {*

   231   Due to Java Applet security restrictions this menu is only available

   232   in the full application version. The meaning of the menu items is as

   233   follows:

   234

   235   \begin{description}

   236

   237   \item[Open \dots] Open a new graph file.

   238

   239   \item[Export to PostScript] Outputs the current graph in Postscript

   240   format, appropriately scaled to fit on one single sheet of A4 paper.

   241   The resulting file can be printed directly.

   242

   243   \item[Export to EPS] Outputs the current graph in Encapsulated

   244   Postscript format. The resulting file can be included in other

   245   documents.

   246

   247   \item[Quit] Quit the graph browser.

   248

   249   \end{description}

   250 *}

   251

   252

   253 subsection {* Syntax of graph definition files *}

   254

   255 text {*

   256   A graph definition file has the following syntax:

   257

   258   \begin{center}\small

   259   \begin{tabular}{rcl}

   260     @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\

   261     @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}

   262   \end{tabular}

   263   \end{center}

   264

   265   The meaning of the items in a vertex description is as follows:

   266

   267   \begin{description}

   268

   269   \item[@{text vertex_name}] The name of the vertex.

   270

   271   \item[@{text vertex_ID}] The vertex identifier. Note that there may

   272   be several vertices with equal names, whereas identifiers must be

   273   unique.

   274

   275   \item[@{text dir_name}] The name of the directory'' the vertex

   276   should be placed in.  A @{verbatim "+"}'' sign after @{text

   277   dir_name} indicates that the nodes in the directory are initially

   278   visible. Directories are initially invisible by default.

   279

   280   \item[@{text path}] The path of the corresponding theory file. This

   281   is specified relatively to the path of the graph definition file.

   282

   283   \item[List of successor/predecessor nodes] A @{verbatim "<"}''

   284   sign before the list means that successor nodes are listed, a

   285   @{verbatim ">"}'' sign means that predecessor nodes are listed. If

   286   neither @{verbatim "<"}'' nor @{verbatim ">"}'' is found, the

   287   browser assumes that successor nodes are listed.

   288

   289   \end{description}

   290 *}

   291

   292 end