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