doc-src/System/Thy/Scala.thy
changeset 47825 4f25960417ae
child 48602 342ca8f3197b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/System/Thy/Scala.thy	Sat Apr 28 17:50:42 2012 +0200
     1.3 @@ -0,0 +1,71 @@
     1.4 +theory Scala
     1.5 +imports Base
     1.6 +begin
     1.7 +
     1.8 +chapter {* Isabelle/Scala development tools *}
     1.9 +
    1.10 +text {* Isabelle/ML and Isabelle/Scala are the two main language
    1.11 +environments for Isabelle tool implementations.  There are some basic
    1.12 +command-line tools to work with the underlying Java Virtual Machine,
    1.13 +the Scala toplevel and compiler.  Note that Isabelle/jEdit
    1.14 +(\secref{sec:tool-tty}) provides a Scala Console for interactive
    1.15 +experimentation within the running application. *}
    1.16 +
    1.17 +
    1.18 +section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *}
    1.19 +
    1.20 +text {* The Isabelle @{tool_def java} utility is a direct wrapper for
    1.21 +  the Java Runtime Environment, within the regular Isabelle settings
    1.22 +  environment (\secref{sec:settings}).  The command line arguments are
    1.23 +  that of the underlying Java version.  It is run in @{verbatim
    1.24 +  "-server"} mode if possible, to improve performance (at the cost of
    1.25 +  extra startup time).
    1.26 +
    1.27 +  The @{verbatim java} executable is the one within @{setting
    1.28 +  ISABELLE_JDK_HOME}, according to the standard directory layout for
    1.29 +  official JDK distributions.  The class loader is augmented such that
    1.30 +  the name space of @{verbatim "Isabelle/Pure.jar"} is available,
    1.31 +  which is the main Isabelle/Scala module.
    1.32 +
    1.33 +  For example, the following command-line invokes the main method of
    1.34 +  class @{verbatim isabelle.GUI_Setup}, which opens a windows with
    1.35 +  some diagnostic information about the Isabelle environment:
    1.36 +\begin{alltt}
    1.37 +  isabelle java isabelle.GUI_Setup
    1.38 +\end{alltt}
    1.39 +*}
    1.40 +
    1.41 +
    1.42 +section {* Scala toplevel \label{sec:tool-scala} *}
    1.43 +
    1.44 +text {* The Isabelle @{tool_def scala} utility is a direct wrapper for
    1.45 +  the Scala toplevel; see also @{tool java} above.  The command line
    1.46 +  arguments are that of the underlying Scala version.
    1.47 +
    1.48 +  This allows to interact with Isabelle/Scala in TTY mode like this:
    1.49 +\begin{alltt}
    1.50 +  isabelle scala
    1.51 +  scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
    1.52 +  scala> isabelle.Isabelle_System.find_logics()
    1.53 +\end{alltt}
    1.54 +*}
    1.55 +
    1.56 +
    1.57 +section {* Scala compiler \label{sec:tool-scalac} *}
    1.58 +
    1.59 +text {* The Isabelle @{tool_def scalac} utility is a direct wrapper
    1.60 +  for the Scala compiler; see also @{tool scala} above.  The command
    1.61 +  line arguments are that of the underlying Scala version.
    1.62 +
    1.63 +  This allows to compile further Scala modules, depending on existing
    1.64 +  Isabelle/Scala functionality.  The resulting class or jar files can
    1.65 +  be added to the @{setting CLASSPATH} via the @{verbatim classpath}
    1.66 +  Bash function that is provided by the Isabelle process environment.
    1.67 +  Thus add-on components can register themselves in a modular manner,
    1.68 +  see also \secref{sec:components}.
    1.69 +
    1.70 +  Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
    1.71 +  adding plugin components, which needs special attention since
    1.72 +  it overrides the standard Java class loader.  *}
    1.73 +
    1.74 +end