6 |
6 |
7 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *} |
7 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *} |
8 |
8 |
9 text {* The @{tool_def jedit} tool invokes a version of |
9 text {* The @{tool_def jedit} tool invokes a version of |
10 jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented |
10 jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented |
11 with some components to provide a fully-featured Prover IDE: |
11 with some plugins to provide a fully-featured Prover IDE: |
12 \begin{ttbox} Usage: isabelle jedit [OPTIONS] |
12 \begin{ttbox} Usage: isabelle jedit [OPTIONS] |
13 [FILES ...] |
13 [FILES ...] |
14 |
14 |
15 Options are: |
15 Options are: |
16 -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) |
16 -J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS) |
35 By default, the specified image is checked and built on demand, see |
35 By default, the specified image is checked and built on demand, see |
36 also @{tool build_dialog}. The @{verbatim "-s"} determines where to |
36 also @{tool build_dialog}. The @{verbatim "-s"} determines where to |
37 store the result session image (see also \secref{sec:tool-build}). |
37 store the result session image (see also \secref{sec:tool-build}). |
38 The @{verbatim "-n"} option bypasses the session build dialog. |
38 The @{verbatim "-n"} option bypasses the session build dialog. |
39 |
39 |
40 The @{verbatim "-m"} option specifies additional print modes. |
40 The @{verbatim "-m"} option specifies additional print modes for the |
|
41 prover process. |
41 |
42 |
42 The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass |
43 The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass |
43 additional low-level options to the JVM or jEdit, respectively. The |
44 additional low-level options to the JVM or jEdit, respectively. The |
44 defaults are provided by the Isabelle settings environment |
45 defaults are provided by the Isabelle settings environment |
45 (\secref{sec:settings}). |
46 (\secref{sec:settings}). |
59 text {* The @{tool_def emacs} tool invokes a version of Emacs and |
60 text {* The @{tool_def emacs} tool invokes a version of Emacs and |
60 Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the |
61 Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the |
61 regular Isabelle settings environment (\secref{sec:settings}). This |
62 regular Isabelle settings environment (\secref{sec:settings}). This |
62 is more convenient than starting Emacs separately, loading the Proof |
63 is more convenient than starting Emacs separately, loading the Proof |
63 General LISP files, and then attempting to start Isabelle with |
64 General LISP files, and then attempting to start Isabelle with |
64 dynamic @{setting PATH} lookup etc. |
65 dynamic @{setting PATH} lookup etc., although it might fail if a |
|
66 different version of Proof General is already part of the Emacs |
|
67 installation of the operating system. |
65 |
68 |
66 The actual interface script is part of the Proof General |
69 The actual interface script is part of the Proof General |
67 distribution; its usage depends on the particular version. There |
70 distribution; its usage depends on the particular version. There |
68 are some options available, such as @{verbatim "-l"} for passing the |
71 are some options available, such as @{verbatim "-l"} for passing the |
69 logic image to be used by default, or @{verbatim "-m"} to tune the |
72 logic image to be used by default, or @{verbatim "-m"} to tune the |
70 standard print mode. The following Isabelle settings are |
73 standard print mode of the prover process. The following Isabelle |
71 particularly important for Proof General: |
74 settings are particularly important for Proof General: |
72 |
75 |
73 \begin{description} |
76 \begin{description} |
74 |
77 |
75 \item[@{setting_def PROOFGENERAL_HOME}] points to the main |
78 \item[@{setting_def PROOFGENERAL_HOME}] points to the main |
76 installation directory of the Proof General distribution. This is |
79 installation directory of the Proof General distribution. This is |