# HG changeset patch # User wenzelm # Date 1335628242 -7200 # Node ID 4f25960417aebe3ef2b6516b0360d6807bfc90f4 # Parent 65082431af2a6978b70d16d69dfa6c6540e7fcbe some coverage of Isabelle/Scala tools; diff -r 65082431af2a -r 4f25960417ae doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Sat Apr 28 17:05:31 2012 +0200 +++ b/doc-src/System/IsaMakefile Sat Apr 28 17:50:42 2012 +0200 @@ -21,8 +21,9 @@ Pure-System: $(LOG)/Pure-System.gz -$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Base.thy Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy +$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy \ + Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy \ + Thy/Scala.thy @$(USEDIR) -s System Pure Thy @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ Thy/document/pdfsetup.sty Thy/document/session.tex diff -r 65082431af2a -r 4f25960417ae doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Sat Apr 28 17:05:31 2012 +0200 +++ b/doc-src/System/Thy/ROOT.ML Sat Apr 28 17:50:42 2012 +0200 @@ -1,1 +1,1 @@ -use_thys ["Basics", "Interfaces", "Presentation", "Misc"]; +use_thys ["Basics", "Interfaces", "Scala", "Presentation", "Misc"]; diff -r 65082431af2a -r 4f25960417ae doc-src/System/Thy/Scala.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Scala.thy Sat Apr 28 17:50:42 2012 +0200 @@ -0,0 +1,71 @@ +theory Scala +imports Base +begin + +chapter {* Isabelle/Scala development tools *} + +text {* Isabelle/ML and Isabelle/Scala are the two main language +environments for Isabelle tool implementations. There are some basic +command-line tools to work with the underlying Java Virtual Machine, +the Scala toplevel and compiler. Note that Isabelle/jEdit +(\secref{sec:tool-tty}) provides a Scala Console for interactive +experimentation within the running application. *} + + +section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *} + +text {* The Isabelle @{tool_def java} utility is a direct wrapper for + the Java Runtime Environment, within the regular Isabelle settings + environment (\secref{sec:settings}). The command line arguments are + that of the underlying Java version. It is run in @{verbatim + "-server"} mode if possible, to improve performance (at the cost of + extra startup time). + + The @{verbatim java} executable is the one within @{setting + ISABELLE_JDK_HOME}, according to the standard directory layout for + official JDK distributions. The class loader is augmented such that + the name space of @{verbatim "Isabelle/Pure.jar"} is available, + which is the main Isabelle/Scala module. + + For example, the following command-line invokes the main method of + class @{verbatim isabelle.GUI_Setup}, which opens a windows with + some diagnostic information about the Isabelle environment: +\begin{alltt} + isabelle java isabelle.GUI_Setup +\end{alltt} +*} + + +section {* Scala toplevel \label{sec:tool-scala} *} + +text {* The Isabelle @{tool_def scala} utility is a direct wrapper for + the Scala toplevel; see also @{tool java} above. The command line + arguments are that of the underlying Scala version. + + This allows to interact with Isabelle/Scala in TTY mode like this: +\begin{alltt} + isabelle scala + scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") + scala> isabelle.Isabelle_System.find_logics() +\end{alltt} +*} + + +section {* Scala compiler \label{sec:tool-scalac} *} + +text {* The Isabelle @{tool_def scalac} utility is a direct wrapper + for the Scala compiler; see also @{tool scala} above. The command + line arguments are that of the underlying Scala version. + + This allows to compile further Scala modules, depending on existing + Isabelle/Scala functionality. The resulting class or jar files can + be added to the @{setting CLASSPATH} via the @{verbatim classpath} + Bash function that is provided by the Isabelle process environment. + Thus add-on components can register themselves in a modular manner, + see also \secref{sec:components}. + + Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for + adding plugin components, which needs special attention since + it overrides the standard Java class loader. *} + +end diff -r 65082431af2a -r 4f25960417ae doc-src/System/Thy/document/Interfaces.tex --- a/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 17:05:31 2012 +0200 +++ b/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 17:50:42 2012 +0200 @@ -94,7 +94,7 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Isabelle/jEdit Prover IDE% +\isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}% } \isamarkuptrue% % diff -r 65082431af2a -r 4f25960417ae doc-src/System/Thy/document/Scala.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/document/Scala.tex Sat Apr 28 17:50:42 2012 +0200 @@ -0,0 +1,118 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Scala}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Scala\isanewline +\isakeyword{imports}\ Base\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Isabelle/Scala development tools% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle/ML and Isabelle/Scala are the two main language +environments for Isabelle tool implementations. There are some basic +command-line tools to work with the underlying Java Virtual Machine, +the Scala toplevel and compiler. Note that Isabelle/jEdit +(\secref{sec:tool-tty}) provides a Scala Console for interactive +experimentation within the running application.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for + the Java Runtime Environment, within the regular Isabelle settings + environment (\secref{sec:settings}). The command line arguments are + that of the underlying Java version. It is run in \verb|-server| mode if possible, to improve performance (at the cost of + extra startup time). + + 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 + official JDK distributions. The class loader is augmented such that + the name space of \verb|Isabelle/Pure.jar| is available, + which is the main Isabelle/Scala module. + + For example, the following command-line invokes the main method of + class \verb|isabelle.GUI_Setup|, which opens a windows with + some diagnostic information about the Isabelle environment: +\begin{alltt} + isabelle java isabelle.GUI_Setup +\end{alltt}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Scala toplevel \label{sec:tool-scala}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for + the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above. The command line + arguments are that of the underlying Scala version. + + This allows to interact with Isabelle/Scala in TTY mode like this: +\begin{alltt} + isabelle scala + scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") + scala> isabelle.Isabelle_System.find_logics() +\end{alltt}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Scala compiler \label{sec:tool-scalac}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper + for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above. The command + line arguments are that of the underlying Scala version. + + This allows to compile further Scala modules, depending on existing + Isabelle/Scala functionality. The resulting class or jar files can + be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath| + Bash function that is provided by the Isabelle process environment. + Thus add-on components can register themselves in a modular manner, + see also \secref{sec:components}. + + Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for + adding plugin components, which needs special attention since + it overrides the standard Java class loader.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 65082431af2a -r 4f25960417ae doc-src/System/system.tex --- a/doc-src/System/system.tex Sat Apr 28 17:05:31 2012 +0200 +++ b/doc-src/System/system.tex Sat Apr 28 17:50:42 2012 +0200 @@ -31,6 +31,7 @@ \input{Thy/document/Basics.tex} \input{Thy/document/Interfaces.tex} \input{Thy/document/Presentation.tex} +\input{Thy/document/Scala.tex} \input{Thy/document/Misc.tex} \begingroup diff -r 65082431af2a -r 4f25960417ae doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Sat Apr 28 17:05:31 2012 +0200 +++ b/doc-src/antiquote_setup.ML Sat Apr 28 17:50:42 2012 +0200 @@ -149,7 +149,8 @@ in defined thy o intern thy end; fun check_tool name = - File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name)); + let val tool_dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"] + in exists (fn dir => File.exists (Path.append dir (Path.basic name))) tool_dirs end; val arg = enclose "{" "}" o clean_string;