author | wenzelm |
Sat, 28 Apr 2012 17:05:31 +0200 | |
changeset 47824 | 65082431af2a |
parent 47822 | 34b44d28fc4b |
child 47826 | 7c97bfe3a501 |
permissions | -rw-r--r-- |
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 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
7 |
section {* Plain TTY interaction \label{sec:tool-tty} *} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
8 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
9 |
text {* |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
10 |
The @{tool_def tty} tool runs the Isabelle process interactively |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
11 |
within a plain terminal session: |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
12 |
\begin{ttbox} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
13 |
Usage: tty [OPTIONS] |
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: |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
16 |
-l NAME logic image name (default ISABELLE_LOGIC) |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
17 |
-m MODE add print mode for output |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
18 |
-p NAME line editor program name (default ISABELLE_LINE_EDITOR) |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
19 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
20 |
Run Isabelle process with plain tty interaction, and optional line editor. |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
21 |
\end{ttbox} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
22 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
23 |
The @{verbatim "-l"} option specifies the logic image. The |
47824 | 24 |
@{verbatim "-m"} option specifies additional print modes. The |
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
25 |
@{verbatim "-p"} option specifies an alternative line editor (such |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
26 |
as the @{executable_def rlwrap} wrapper for GNU readline); the |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
27 |
fall-back is to use raw standard input. |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
28 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
29 |
Regular interaction is via the standard Isabelle/Isar toplevel loop. |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
30 |
The Isar command @{command exit} drops out into the raw ML system, |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
31 |
which is occasionally useful for low-level debugging. Invoking @{ML |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
32 |
Isar.loop}~@{verbatim "();"} in ML will return to the Isar toplevel. |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
33 |
*} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
34 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
35 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
36 |
section {* Proof General / Emacs *} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
37 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
38 |
text {* |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
39 |
The @{tool_def emacs} tool invokes a version of Emacs and Proof |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
40 |
General within the regular Isabelle settings environment |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
41 |
(\secref{sec:settings}). This is more robust than starting Emacs |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
42 |
separately, loading the Proof General lisp files, and then |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
43 |
attempting to start Isabelle with dynamic @{setting PATH} lookup |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
44 |
etc. |
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 |
The actual interface script is part of the Proof General |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
47 |
distribution~\cite{proofgeneral}; its usage depends on the |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
48 |
particular version. There are some options available, such as |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
49 |
@{verbatim "-l"} for passing the logic image to be used by default, |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
50 |
or @{verbatim "-m"} to tune the standard print mode. The following |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
51 |
Isabelle settings are particularly important for Proof General: |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
52 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
53 |
\begin{description} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
54 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
55 |
\item[@{setting_def PROOFGENERAL_HOME}] points to the main |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
56 |
installation directory of the Proof General distribution. The |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
57 |
default settings try to locate this in a number of standard places, |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
58 |
notably @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}. |
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 |
\item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
61 |
the command line of any invocation of the Proof General @{verbatim |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
62 |
interface} script. |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
63 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
64 |
\item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell |
47822
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
65 |
script to install the X11 fonts required for the old X-Symbols mode |
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
66 |
of Proof General. This is only relevant if the X11 display server |
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
67 |
runs on a different machine than the Emacs application, with a |
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
68 |
different file-system view on the Proof General installation. Under |
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
69 |
most circumstances Proof General 3.x is able to refer to the font |
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
70 |
files that are part of its distribution, and Proof General 4.x finds |
34b44d28fc4b
some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
wenzelm
parents:
43564
diff
changeset
|
71 |
its fonts by different means. |
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
72 |
|
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
73 |
\end{description} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
74 |
*} |
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
75 |
|
47824 | 76 |
|
77 |
section {* Isabelle/jEdit Prover IDE *} |
|
78 |
||
79 |
text {* The @{tool_def jedit} tool invokes a version of jEdit that has |
|
80 |
been augmented with some components to provide a fully-featured |
|
81 |
Prover IDE (based on Isabelle/Scala): |
|
82 |
\begin{ttbox} |
|
83 |
Usage: isabelle jedit [OPTIONS] [FILES ...] |
|
84 |
||
85 |
Options are: |
|
86 |
-J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) |
|
87 |
-b build only |
|
88 |
-d enable debugger |
|
89 |
-f fresh build |
|
90 |
-j OPTION add jEdit runtime option (default JEDIT_OPTIONS) |
|
91 |
-l NAME logic image name (default ISABELLE_LOGIC) |
|
92 |
-m MODE add print mode for output |
|
93 |
||
94 |
Start jEdit with Isabelle plugin setup and opens theory FILES |
|
95 |
(default Scratch.thy). |
|
96 |
\end{ttbox} |
|
97 |
||
98 |
The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass |
|
99 |
additional low-level options to the JVM or jEdit, respectively. The |
|
100 |
defaults are provided by the Isabelle settings environment. |
|
101 |
||
102 |
The @{verbatim "-d"} option allows to connect to the runtime debugger |
|
103 |
of the JVM. Note that the Scala Console of Isabelle/jEdit is more |
|
104 |
convenient in most practical situations. |
|
105 |
||
106 |
The @{verbatim "-b"} and @{verbatim "-f"} options control the |
|
107 |
self-build mechanism of Isabelle/jEdit. This is only relevant for |
|
108 |
building from sources, which also requires an auxiliary @{verbatim |
|
109 |
jedit_build} component. Official Isabelle releases already include a |
|
110 |
version of Isabelle/jEdit that is built properly. |
|
111 |
||
112 |
The @{verbatim "-l"} option specifies the logic image. The |
|
113 |
@{verbatim "-m"} option specifies additional print modes. |
|
114 |
*} |
|
115 |
||
28916
0a802cdda340
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
diff
changeset
|
116 |
end |