doc-src/System/Thy/Interfaces.thy
author wenzelm
Mon, 30 Jul 2012 14:29:12 +0200
changeset 48603 a37463482e5f
parent 48602 342ca8f3197b
child 48791 9e8f30bfbdca
permissions -rw-r--r--
discontinued unused isabelle jedit debugger; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
     1
theory Interfaces
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 32088
diff changeset
     2
imports Base
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
     3
begin
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
     4
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
     5
chapter {* User interfaces *}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
     6
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
     7
section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
     8
48603
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
     9
text {* The @{tool_def jedit} tool invokes a version of
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    10
  jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    11
  with some components to provide a fully-featured Prover IDE:
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    12
\begin{ttbox} Usage: isabelle jedit [OPTIONS]
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    13
  [FILES ...]
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    14
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    15
  Options are:
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    16
    -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    17
    -b           build only
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    18
    -f           fresh build
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    19
    -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    20
    -l NAME      logic image name (default ISABELLE_LOGIC)
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    21
    -m MODE      add print mode for output
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    22
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    23
Start jEdit with Isabelle plugin setup and opens theory FILES
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    24
(default Scratch.thy).
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    25
\end{ttbox}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    26
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    27
  The @{verbatim "-l"} option specifies the logic image.  The
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    28
  @{verbatim "-m"} option specifies additional print modes.
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    29
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    30
  The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    31
  additional low-level options to the JVM or jEdit, respectively.  The
48603
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    32
  defaults are provided by the Isabelle settings environment
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    33
  (\secref{sec:settings}).
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    34
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    35
  The @{verbatim "-b"} and @{verbatim "-f"} options control the
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    36
  self-build mechanism of Isabelle/jEdit.  This is only relevant for
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    37
  building from sources, which also requires an auxiliary @{verbatim
48603
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    38
  jedit_build}
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    39
  component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    40
  that official Isabelle releases already include a version of
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    41
  Isabelle/jEdit that is built properly.  *}
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    42
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    43
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    44
section {* Proof General / Emacs *}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    45
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    46
text {* The @{tool_def emacs} tool invokes a version of Emacs and
48603
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    47
  Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    48
  regular Isabelle settings environment (\secref{sec:settings}).  This
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    49
  is more convenient than starting Emacs separately, loading the Proof
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    50
  General LISP files, and then attempting to start Isabelle with
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    51
  dynamic @{setting PATH} lookup etc.
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    52
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    53
  The actual interface script is part of the Proof General
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    54
  distribution; its usage depends on the particular version.  There
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    55
  are some options available, such as @{verbatim "-l"} for passing the
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    56
  logic image to be used by default, or @{verbatim "-m"} to tune the
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    57
  standard print mode.  The following Isabelle settings are
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    58
  particularly important for Proof General:
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    59
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    60
  \begin{description}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    61
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    62
  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    63
  installation directory of the Proof General distribution.  This is
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    64
  implicitly provided for versions of Proof General that are
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    65
  distributed as Isabelle component, see also \secref{sec:components};
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    66
  otherwise it needs to be configured manually.
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    67
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    68
  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    69
  the command line of any invocation of the Proof General @{verbatim
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    70
  interface} script.  This allows to provide persistent default
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    71
  options for the invocation of \texttt{isabelle emacs}.
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    72
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    73
  \end{description}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    74
*}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    75
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    76
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    77
section {* Plain TTY interaction \label{sec:tool-tty} *}
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    78
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    79
text {*
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    80
  The @{tool_def tty} tool runs the Isabelle process interactively
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    81
  within a plain terminal session:
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    82
\begin{ttbox}
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    83
Usage: isabelle tty [OPTIONS]
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    84
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    85
  Options are:
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    86
    -l NAME      logic image name (default ISABELLE_LOGIC)
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    87
    -m MODE      add print mode for output
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    88
    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    89
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    90
  Run Isabelle process with plain tty interaction and line editor.
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    91
\end{ttbox}
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    92
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    93
  The @{verbatim "-l"} option specifies the logic image.  The
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    94
  @{verbatim "-m"} option specifies additional print modes.  The
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    95
  @{verbatim "-p"} option specifies an alternative line editor (such
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    96
  as the @{executable_def rlwrap} wrapper for GNU readline); the
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    97
  fall-back is to use raw standard input.
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    98
48603
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
    99
  Regular interaction works via the standard Isabelle/Isar toplevel
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
   100
  loop.  The Isar command @{command exit} drops out into the
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
   101
  bare-bones ML system, which is occasionally useful for debugging of
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
   102
  the Isar infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim
a37463482e5f discontinued unused isabelle jedit debugger;
wenzelm
parents: 48602
diff changeset
   103
  "();"} in ML will return to the Isar toplevel.  *}
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
   104
48576
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   105
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   106
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   107
section {* Theory graph browser \label{sec:browse} *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   108
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   109
text {* The Isabelle graph browser is a general tool for visualizing
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   110
  dependency graphs.  Certain nodes of the graph (i.e.\ theories) can
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   111
  be grouped together in ``directories'', whose contents may be
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   112
  hidden, thus enabling the user to collapse irrelevant portions of
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   113
  information.  The browser is written in Java, it can be used both as
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   114
  a stand-alone application and as an applet.  Note that the option
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48576
diff changeset
   115
  @{verbatim "-g"} of @{tool_ref usedir} creates graph presentations
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48576
diff changeset
   116
  in batch mode for inclusion in session documents.  *}
48576
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   117
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   118
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   119
subsection {* Invoking the graph browser *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   120
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48576
diff changeset
   121
text {* The stand-alone version of the graph browser is wrapped up as
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48576
diff changeset
   122
  @{tool_def browser}:
48576
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   123
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48576
diff changeset
   124
Usage: isabelle browser [OPTIONS] [GRAPHFILE]
48576
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   125
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   126
  Options are:
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   127
    -b           Admin/build only
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   128
    -c           cleanup -- remove GRAPHFILE after use
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   129
    -o FILE      output to FILE (ps, eps, pdf)
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   130
\end{ttbox}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   131
  When no filename is specified, the browser automatically changes to
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   132
  the directory @{setting ISABELLE_BROWSER_INFO}.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   133
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   134
  \medskip The @{verbatim "-b"} option indicates that this is for
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   135
  administrative build only, i.e.\ no browser popup if no files are
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   136
  given.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   137
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   138
  The @{verbatim "-c"} option causes the input file to be removed
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   139
  after use.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   140
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   141
  The @{verbatim "-o"} option indicates batch-mode operation, with the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   142
  output written to the indicated file; note that @{verbatim pdf}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   143
  produces an @{verbatim eps} copy as well.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   144
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   145
  \medskip The applet version of the browser is part of the standard
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   146
  WWW theory presentation, see the link ``theory dependencies'' within
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   147
  each session index.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   148
*}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   149
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   150
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   151
subsection {* Using the graph browser *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   152
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   153
text {*
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   154
  The browser's main window, which is shown in
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   155
  \figref{fig:browserwindow}, consists of two sub-windows.  In the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   156
  left sub-window, the directory tree is displayed. The graph itself
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   157
  is displayed in the right sub-window.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   158
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   159
  \begin{figure}[ht]
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   160
  \includegraphics[width=\textwidth]{browser_screenshot}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   161
  \caption{\label{fig:browserwindow} Browser main window}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   162
  \end{figure}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   163
*}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   164
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   165
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   166
subsubsection {* The directory tree window *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   167
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   168
text {*
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   169
  We describe the usage of the directory browser and the meaning of
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   170
  the different items in the browser window.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   171
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   172
  \begin{itemize}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   173
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   174
  \item A red arrow before a directory name indicates that the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   175
  directory is currently ``folded'', i.e.~the nodes in this directory
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   176
  are collapsed to one single node. In the right sub-window, the names
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   177
  of nodes corresponding to folded directories are enclosed in square
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   178
  brackets and displayed in red color.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   179
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   180
  \item A green downward arrow before a directory name indicates that
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   181
  the directory is currently ``unfolded''. It can be folded by
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   182
  clicking on the directory name.  Clicking on the name for a second
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   183
  time unfolds the directory again.  Alternatively, a directory can
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   184
  also be unfolded by clicking on the corresponding node in the right
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   185
  sub-window.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   186
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   187
  \item Blue arrows stand before ordinary node names. When clicking on
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   188
  such a name (i.e.\ that of a theory), the graph display window
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   189
  focuses to the corresponding node. Double clicking invokes a text
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   190
  viewer window in which the contents of the theory file are
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   191
  displayed.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   192
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   193
  \end{itemize}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   194
*}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   195
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   196
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   197
subsubsection {* The graph display window *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   198
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   199
text {*
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   200
  When pointing on an ordinary node, an upward and a downward arrow is
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   201
  shown.  Initially, both of these arrows are green. Clicking on the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   202
  upward or downward arrow collapses all predecessor or successor
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   203
  nodes, respectively. The arrow's color then changes to red,
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   204
  indicating that the predecessor or successor nodes are currently
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   205
  collapsed. The node corresponding to the collapsed nodes has the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   206
  name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   207
  click on the red arrow or on the node with the name ``@{verbatim
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   208
  "[....]"}''. Similar to the directory browser, the contents of
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   209
  theory files can be displayed by double clicking on the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   210
  corresponding node.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   211
*}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   212
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   213
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   214
subsubsection {* The ``File'' menu *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   215
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   216
text {*
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   217
  Due to Java Applet security restrictions this menu is only available
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   218
  in the full application version. The meaning of the menu items is as
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   219
  follows:
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   220
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   221
  \begin{description}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   222
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   223
  \item[Open \dots] Open a new graph file.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   224
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   225
  \item[Export to PostScript] Outputs the current graph in Postscript
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   226
  format, appropriately scaled to fit on one single sheet of A4 paper.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   227
  The resulting file can be printed directly.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   228
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   229
  \item[Export to EPS] Outputs the current graph in Encapsulated
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   230
  Postscript format. The resulting file can be included in other
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   231
  documents.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   232
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   233
  \item[Quit] Quit the graph browser.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   234
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   235
  \end{description}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   236
*}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   237
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   238
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   239
subsection {* Syntax of graph definition files *}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   240
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   241
text {*
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   242
  A graph definition file has the following syntax:
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   243
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   244
  \begin{center}\small
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   245
  \begin{tabular}{rcl}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   246
    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   247
    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   248
  \end{tabular}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   249
  \end{center}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   250
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   251
  The meaning of the items in a vertex description is as follows:
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   252
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   253
  \begin{description}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   254
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   255
  \item[@{text vertex_name}] The name of the vertex.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   256
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   257
  \item[@{text vertex_ID}] The vertex identifier. Note that there may
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   258
  be several vertices with equal names, whereas identifiers must be
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   259
  unique.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   260
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   261
  \item[@{text dir_name}] The name of the ``directory'' the vertex
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   262
  should be placed in.  A ``@{verbatim "+"}'' sign after @{text
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   263
  dir_name} indicates that the nodes in the directory are initially
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   264
  visible. Directories are initially invisible by default.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   265
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   266
  \item[@{text path}] The path of the corresponding theory file. This
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   267
  is specified relatively to the path of the graph definition file.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   268
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   269
  \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   270
  sign before the list means that successor nodes are listed, a
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   271
  ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   272
  neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   273
  browser assumes that successor nodes are listed.
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   274
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   275
  \end{description}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   276
*}
72c0bf1f544f isabelle browser is another user interface;
wenzelm
parents: 48573
diff changeset
   277
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
   278
end