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