doc-src/System/Thy/Interfaces.thy
author wenzelm
Sat, 28 Jul 2012 13:01:48 +0200
changeset 48573 de82a584bc2a
parent 48572 af0f5560ac94
child 48576 72c0bf1f544f
permissions -rw-r--r--
top-down order of user interfaces;
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
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
     9
text {* The @{tool_def jedit} tool invokes a version of jEdit that has
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    10
  been augmented with some components to provide a fully-featured
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    11
  Prover IDE (based on Isabelle/Scala):
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    12
\begin{ttbox}
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    13
Usage: isabelle jedit [OPTIONS] [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
    -d           enable debugger
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
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    23
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    24
Start jEdit with Isabelle plugin setup and opens theory FILES
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    25
(default Scratch.thy).
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    26
\end{ttbox}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    27
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    28
  The @{verbatim "-l"} option specifies the logic image.  The
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    29
  @{verbatim "-m"} option specifies additional print modes.
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    30
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    31
  The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    32
  additional low-level options to the JVM or jEdit, respectively.  The
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    33
  defaults are provided by the Isabelle settings environment.
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    34
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    35
  The @{verbatim "-d"} option allows to connect to the runtime
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    36
  debugger of the JVM.  Note that the Scala Console of Isabelle/jEdit
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    37
  is more convenient in most practical situations.
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    38
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    39
  The @{verbatim "-b"} and @{verbatim "-f"} options control the
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    40
  self-build mechanism of Isabelle/jEdit.  This is only relevant for
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    41
  building from sources, which also requires an auxiliary @{verbatim
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    42
  jedit_build} component.  Official Isabelle releases already include
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    43
  a version of Isabelle/jEdit that is built properly.
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    44
*}
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    45
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    46
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    47
section {* Proof General / Emacs *}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    48
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    49
text {* The @{tool_def emacs} tool invokes a version of Emacs and
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    50
  Proof General \cite{proofgeneral} within the regular Isabelle
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    51
  settings environment (\secref{sec:settings}).  This is more
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    52
  convenient than starting Emacs separately, loading the Proof General
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    53
  lisp files, and then attempting to start Isabelle with dynamic
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    54
  @{setting PATH} lookup etc.
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    55
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    56
  The actual interface script is part of the Proof General
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    57
  distribution; its usage depends on the particular version.  There
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    58
  are some options available, such as @{verbatim "-l"} for passing the
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    59
  logic image to be used by default, or @{verbatim "-m"} to tune the
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    60
  standard print mode.  The following Isabelle settings are
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    61
  particularly important for Proof General:
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    62
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    63
  \begin{description}
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    64
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    65
  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    66
  installation directory of the Proof General distribution.  This is
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    67
  implicitly provided for versions of Proof General that are
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    68
  distributed as Isabelle component, see also \secref{sec:components};
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    69
  otherwise it needs to be configured manually.
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    70
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    71
  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
    72
  the command line of any invocation of the Proof General @{verbatim
48572
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    73
  interface} script.  This allows to provide persistent default
af0f5560ac94 misc tuning;
wenzelm
parents: 48208
diff changeset
    74
  options for the invocation of \texttt{isabelle emacs}.
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
  \end{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
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    79
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    80
section {* Plain TTY interaction \label{sec:tool-tty} *}
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    81
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    82
text {*
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    83
  The @{tool_def tty} tool runs the Isabelle process interactively
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    84
  within a plain terminal session:
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    85
\begin{ttbox}
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    86
Usage: isabelle tty [OPTIONS]
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    87
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    88
  Options are:
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    89
    -l NAME      logic image name (default ISABELLE_LOGIC)
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    90
    -m MODE      add print mode for output
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    91
    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
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
  Run Isabelle process with plain tty interaction and line editor.
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
    94
\end{ttbox}
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
  The @{verbatim "-l"} option specifies the logic image.  The
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    97
  @{verbatim "-m"} option specifies additional print modes.  The
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    98
  @{verbatim "-p"} option specifies an alternative line editor (such
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
    99
  as the @{executable_def rlwrap} wrapper for GNU readline); the
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
   100
  fall-back is to use raw standard input.
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
   101
48573
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
   102
  Regular interaction is via the standard Isabelle/Isar toplevel loop.
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
   103
  The Isar command @{command exit} drops out into the bare-bones ML
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
   104
  system, which is occasionally useful for debugging of the Isar
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
   105
  infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim "();"}
de82a584bc2a top-down order of user interfaces;
wenzelm
parents: 48572
diff changeset
   106
  in ML will return to the Isar toplevel.  *}
47824
65082431af2a some coverage of Isabelle/jEdit;
wenzelm
parents: 47822
diff changeset
   107
28916
0a802cdda340 removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff changeset
   108
end