doc-src/System/Thy/Interfaces.thy

 
 chapter {* User interfaces *}
 
 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
 
-text {* The @{tool_def jedit} tool invokes a version of jEdit that has
-  been augmented with some components to provide a fully-featured
-  Prover IDE (based on Isabelle/Scala):
-\begin{ttbox}
-Usage: isabelle jedit [OPTIONS] [FILES ...]
+text {* The @{tool_def jedit} tool invokes a version of
+  jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
+  with some components to provide a fully-featured Prover IDE:
+\begin{ttbox} Usage: isabelle jedit [OPTIONS]
+  [FILES ...]
 
   Options are:
     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     -b           build only
-    -d           enable debugger
     -f           fresh build
     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
     -l NAME      logic image name (default ISABELLE_LOGIC)
     -m MODE      add print mode for output
 

   The @{verbatim "-l"} option specifies the logic image.  The
   @{verbatim "-m"} option specifies additional print modes.
 
   The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
   additional low-level options to the JVM or jEdit, respectively.  The
-  defaults are provided by the Isabelle settings environment.
-
-  The @{verbatim "-d"} option allows to connect to the runtime
-  debugger of the JVM.  Note that the Scala Console of Isabelle/jEdit
-  is more convenient in most practical situations.
+  defaults are provided by the Isabelle settings environment
+  (\secref{sec:settings}).
 
   The @{verbatim "-b"} and @{verbatim "-f"} options control the
   self-build mechanism of Isabelle/jEdit.  This is only relevant for
   building from sources, which also requires an auxiliary @{verbatim
-  jedit_build} component.  Official Isabelle releases already include
-  a version of Isabelle/jEdit that is built properly.
-*}
+  jedit_build}
+  component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
+  that official Isabelle releases already include a version of
+  Isabelle/jEdit that is built properly.  *}
 
 
 section {* Proof General / Emacs *}
 
 text {* The @{tool_def emacs} tool invokes a version of Emacs and
-  Proof General \cite{proofgeneral} within the regular Isabelle
-  settings environment (\secref{sec:settings}).  This is more
-  convenient than starting Emacs separately, loading the Proof General
-  lisp files, and then attempting to start Isabelle with dynamic
-  @{setting PATH} lookup etc.
+  Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
+  regular Isabelle settings environment (\secref{sec:settings}).  This
+  is more convenient than starting Emacs separately, loading the Proof
+  General LISP files, and then attempting to start Isabelle with
+  dynamic @{setting PATH} lookup etc.
 
   The actual interface script is part of the Proof General
   distribution; its usage depends on the particular version.  There
   are some options available, such as @{verbatim "-l"} for passing the
   logic image to be used by default, or @{verbatim "-m"} to tune the

   @{verbatim "-m"} option specifies additional print modes.  The
   @{verbatim "-p"} option specifies an alternative line editor (such
   as the @{executable_def rlwrap} wrapper for GNU readline); the
   fall-back is to use raw standard input.
 
-  Regular interaction is via the standard Isabelle/Isar toplevel loop.
-  The Isar command @{command exit} drops out into the bare-bones ML
-  system, which is occasionally useful for debugging of the Isar
-  infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim "();"}
-  in ML will return to the Isar toplevel.  *}
+  Regular interaction works via the standard Isabelle/Isar toplevel
+  loop.  The Isar command @{command exit} drops out into the
+  bare-bones ML system, which is occasionally useful for debugging of
+  the Isar infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim
+  "();"} in ML will return to the Isar toplevel.  *}
 
 
 
 section {* Theory graph browser \label{sec:browse} *}