doc-src/System/Thy/document/Scala.tex
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/document/Scala.tex	Sat Apr 28 17:50:42 2012 +0200
     1.3 @@ -0,0 +1,118 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{Scala}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +%
    1.10 +\endisadelimtheory
    1.11 +%
    1.12 +\isatagtheory
    1.13 +\isacommand{theory}\isamarkupfalse%
    1.14 +\ Scala\isanewline
    1.15 +\isakeyword{imports}\ Base\isanewline
    1.16 +\isakeyword{begin}%
    1.17 +\endisatagtheory
    1.18 +{\isafoldtheory}%
    1.19 +%
    1.20 +\isadelimtheory
    1.21 +%
    1.22 +\endisadelimtheory
    1.23 +%
    1.24 +\isamarkupchapter{Isabelle/Scala development tools%
    1.25 +}
    1.26 +\isamarkuptrue%
    1.27 +%
    1.28 +\begin{isamarkuptext}%
    1.29 +Isabelle/ML and Isabelle/Scala are the two main language
    1.30 +environments for Isabelle tool implementations.  There are some basic
    1.31 +command-line tools to work with the underlying Java Virtual Machine,
    1.32 +the Scala toplevel and compiler.  Note that Isabelle/jEdit
    1.33 +(\secref{sec:tool-tty}) provides a Scala Console for interactive
    1.34 +experimentation within the running application.%
    1.35 +\end{isamarkuptext}%
    1.36 +\isamarkuptrue%
    1.37 +%
    1.38 +\isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}%
    1.39 +}
    1.40 +\isamarkuptrue%
    1.41 +%
    1.42 +\begin{isamarkuptext}%
    1.43 +The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for
    1.44 +  the Java Runtime Environment, within the regular Isabelle settings
    1.45 +  environment (\secref{sec:settings}).  The command line arguments are
    1.46 +  that of the underlying Java version.  It is run in \verb|-server| mode if possible, to improve performance (at the cost of
    1.47 +  extra startup time).
    1.48 +
    1.49 +  The \verb|java| executable is the one within \hyperlink{setting.ISABELLE-JDK-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}JDK{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, according to the standard directory layout for
    1.50 +  official JDK distributions.  The class loader is augmented such that
    1.51 +  the name space of \verb|Isabelle/Pure.jar| is available,
    1.52 +  which is the main Isabelle/Scala module.
    1.53 +
    1.54 +  For example, the following command-line invokes the main method of
    1.55 +  class \verb|isabelle.GUI_Setup|, which opens a windows with
    1.56 +  some diagnostic information about the Isabelle environment:
    1.57 +\begin{alltt}
    1.58 +  isabelle java isabelle.GUI_Setup
    1.59 +\end{alltt}%
    1.60 +\end{isamarkuptext}%
    1.61 +\isamarkuptrue%
    1.62 +%
    1.63 +\isamarkupsection{Scala toplevel \label{sec:tool-scala}%
    1.64 +}
    1.65 +\isamarkuptrue%
    1.66 +%
    1.67 +\begin{isamarkuptext}%
    1.68 +The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for
    1.69 +  the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above.  The command line
    1.70 +  arguments are that of the underlying Scala version.
    1.71 +
    1.72 +  This allows to interact with Isabelle/Scala in TTY mode like this:
    1.73 +\begin{alltt}
    1.74 +  isabelle scala
    1.75 +  scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
    1.76 +  scala> isabelle.Isabelle_System.find_logics()
    1.77 +\end{alltt}%
    1.78 +\end{isamarkuptext}%
    1.79 +\isamarkuptrue%
    1.80 +%
    1.81 +\isamarkupsection{Scala compiler \label{sec:tool-scalac}%
    1.82 +}
    1.83 +\isamarkuptrue%
    1.84 +%
    1.85 +\begin{isamarkuptext}%
    1.86 +The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper
    1.87 +  for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above.  The command
    1.88 +  line arguments are that of the underlying Scala version.
    1.89 +
    1.90 +  This allows to compile further Scala modules, depending on existing
    1.91 +  Isabelle/Scala functionality.  The resulting class or jar files can
    1.92 +  be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath|
    1.93 +  Bash function that is provided by the Isabelle process environment.
    1.94 +  Thus add-on components can register themselves in a modular manner,
    1.95 +  see also \secref{sec:components}.
    1.96 +
    1.97 +  Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
    1.98 +  adding plugin components, which needs special attention since
    1.99 +  it overrides the standard Java class loader.%
   1.100 +\end{isamarkuptext}%
   1.101 +\isamarkuptrue%
   1.102 +%
   1.103 +\isadelimtheory
   1.104 +%
   1.105 +\endisadelimtheory
   1.106 +%
   1.107 +\isatagtheory
   1.108 +\isacommand{end}\isamarkupfalse%
   1.109 +%
   1.110 +\endisatagtheory
   1.111 +{\isafoldtheory}%
   1.112 +%
   1.113 +\isadelimtheory
   1.114 +%
   1.115 +\endisadelimtheory
   1.116 +\isanewline
   1.117 +\end{isabellebody}%
   1.118 +%%% Local Variables:
   1.119 +%%% mode: latex
   1.120 +%%% TeX-master: "root"
   1.121 +%%% End: