some coverage of Isabelle/jEdit;
authorwenzelm
Sat Apr 28 17:05:31 2012 +0200 (2012-04-28)
changeset 4782465082431af2a
parent 47823 4fad76e6f4ba
child 47825 4f25960417ae
some coverage of Isabelle/jEdit;
doc-src/System/Thy/Interfaces.thy
doc-src/System/Thy/document/Interfaces.tex
     1.1 --- a/doc-src/System/Thy/Interfaces.thy	Sat Apr 28 16:44:32 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Interfaces.thy	Sat Apr 28 17:05:31 2012 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  \end{ttbox}
     1.5  
     1.6    The @{verbatim "-l"} option specifies the logic image.  The
     1.7 -  @{verbatim "-m"} option specifies additional print modes.  The The
     1.8 +  @{verbatim "-m"} option specifies additional print modes.  The
     1.9    @{verbatim "-p"} option specifies an alternative line editor (such
    1.10    as the @{executable_def rlwrap} wrapper for GNU readline); the
    1.11    fall-back is to use raw standard input.
    1.12 @@ -73,4 +73,44 @@
    1.13    \end{description}
    1.14  *}
    1.15  
    1.16 +
    1.17 +section {* Isabelle/jEdit Prover IDE *}
    1.18 +
    1.19 +text {* The @{tool_def jedit} tool invokes a version of jEdit that has
    1.20 +  been augmented with some components to provide a fully-featured
    1.21 +  Prover IDE (based on Isabelle/Scala):
    1.22 +\begin{ttbox}
    1.23 +Usage: isabelle jedit [OPTIONS] [FILES ...]
    1.24 +
    1.25 +  Options are:
    1.26 +    -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
    1.27 +    -b           build only
    1.28 +    -d           enable debugger
    1.29 +    -f           fresh build
    1.30 +    -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    1.31 +    -l NAME      logic image name (default ISABELLE_LOGIC)
    1.32 +    -m MODE      add print mode for output
    1.33 +
    1.34 +Start jEdit with Isabelle plugin setup and opens theory FILES
    1.35 +(default Scratch.thy).
    1.36 +\end{ttbox}
    1.37 +
    1.38 +The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
    1.39 +additional low-level options to the JVM or jEdit, respectively.  The
    1.40 +defaults are provided by the Isabelle settings environment.
    1.41 +
    1.42 +The @{verbatim "-d"} option allows to connect to the runtime debugger
    1.43 +of the JVM.  Note that the Scala Console of Isabelle/jEdit is more
    1.44 +convenient in most practical situations.
    1.45 +
    1.46 +The @{verbatim "-b"} and @{verbatim "-f"} options control the
    1.47 +self-build mechanism of Isabelle/jEdit.  This is only relevant for
    1.48 +building from sources, which also requires an auxiliary @{verbatim
    1.49 +jedit_build} component.  Official Isabelle releases already include a
    1.50 +version of Isabelle/jEdit that is built properly.
    1.51 +
    1.52 +The @{verbatim "-l"} option specifies the logic image.  The
    1.53 +@{verbatim "-m"} option specifies additional print modes.
    1.54 +*}
    1.55 +
    1.56  end
    1.57 \ No newline at end of file
     2.1 --- a/doc-src/System/Thy/document/Interfaces.tex	Sat Apr 28 16:44:32 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Interfaces.tex	Sat Apr 28 17:05:31 2012 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4  \end{ttbox}
     2.5  
     2.6    The \verb|-l| option specifies the logic image.  The
     2.7 -  \verb|-m| option specifies additional print modes.  The The
     2.8 +  \verb|-m| option specifies additional print modes.  The
     2.9    \verb|-p| option specifies an alternative line editor (such
    2.10    as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the
    2.11    fall-back is to use raw standard input.
    2.12 @@ -94,6 +94,48 @@
    2.13  \end{isamarkuptext}%
    2.14  \isamarkuptrue%
    2.15  %
    2.16 +\isamarkupsection{Isabelle/jEdit Prover IDE%
    2.17 +}
    2.18 +\isamarkuptrue%
    2.19 +%
    2.20 +\begin{isamarkuptext}%
    2.21 +The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has
    2.22 +  been augmented with some components to provide a fully-featured
    2.23 +  Prover IDE (based on Isabelle/Scala):
    2.24 +\begin{ttbox}
    2.25 +Usage: isabelle jedit [OPTIONS] [FILES ...]
    2.26 +
    2.27 +  Options are:
    2.28 +    -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
    2.29 +    -b           build only
    2.30 +    -d           enable debugger
    2.31 +    -f           fresh build
    2.32 +    -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    2.33 +    -l NAME      logic image name (default ISABELLE_LOGIC)
    2.34 +    -m MODE      add print mode for output
    2.35 +
    2.36 +Start jEdit with Isabelle plugin setup and opens theory FILES
    2.37 +(default Scratch.thy).
    2.38 +\end{ttbox}
    2.39 +
    2.40 +The \verb|-J| and \verb|-j| options allow to pass
    2.41 +additional low-level options to the JVM or jEdit, respectively.  The
    2.42 +defaults are provided by the Isabelle settings environment.
    2.43 +
    2.44 +The \verb|-d| option allows to connect to the runtime debugger
    2.45 +of the JVM.  Note that the Scala Console of Isabelle/jEdit is more
    2.46 +convenient in most practical situations.
    2.47 +
    2.48 +The \verb|-b| and \verb|-f| options control the
    2.49 +self-build mechanism of Isabelle/jEdit.  This is only relevant for
    2.50 +building from sources, which also requires an auxiliary \verb|jedit_build| component.  Official Isabelle releases already include a
    2.51 +version of Isabelle/jEdit that is built properly.
    2.52 +
    2.53 +The \verb|-l| option specifies the logic image.  The
    2.54 +\verb|-m| option specifies additional print modes.%
    2.55 +\end{isamarkuptext}%
    2.56 +\isamarkuptrue%
    2.57 +%
    2.58  \isadelimtheory
    2.59  %
    2.60  \endisadelimtheory