some coverage of Isabelle/Scala tools;
authorwenzelm
Sat Apr 28 17:50:42 2012 +0200 (2012-04-28)
changeset 478254f25960417ae
parent 47824 65082431af2a
child 47826 7c97bfe3a501
some coverage of Isabelle/Scala tools;
doc-src/System/IsaMakefile
doc-src/System/Thy/ROOT.ML
doc-src/System/Thy/Scala.thy
doc-src/System/Thy/document/Interfaces.tex
doc-src/System/Thy/document/Scala.tex
doc-src/System/system.tex
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/System/IsaMakefile	Sat Apr 28 17:05:31 2012 +0200
     1.2 +++ b/doc-src/System/IsaMakefile	Sat Apr 28 17:50:42 2012 +0200
     1.3 @@ -21,8 +21,9 @@
     1.4  
     1.5  Pure-System: $(LOG)/Pure-System.gz
     1.6  
     1.7 -$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
     1.8 -  Thy/Base.thy Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy
     1.9 +$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
    1.10 +  Thy/Basics.thy Thy/Misc.thy Thy/Interfaces.thy Thy/Presentation.thy	\
    1.11 +  Thy/Scala.thy
    1.12  	@$(USEDIR) -s System Pure Thy
    1.13  	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
    1.14  	 Thy/document/pdfsetup.sty Thy/document/session.tex
     2.1 --- a/doc-src/System/Thy/ROOT.ML	Sat Apr 28 17:05:31 2012 +0200
     2.2 +++ b/doc-src/System/Thy/ROOT.ML	Sat Apr 28 17:50:42 2012 +0200
     2.3 @@ -1,1 +1,1 @@
     2.4 -use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
     2.5 +use_thys ["Basics", "Interfaces", "Scala", "Presentation", "Misc"];
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/System/Thy/Scala.thy	Sat Apr 28 17:50:42 2012 +0200
     3.3 @@ -0,0 +1,71 @@
     3.4 +theory Scala
     3.5 +imports Base
     3.6 +begin
     3.7 +
     3.8 +chapter {* Isabelle/Scala development tools *}
     3.9 +
    3.10 +text {* Isabelle/ML and Isabelle/Scala are the two main language
    3.11 +environments for Isabelle tool implementations.  There are some basic
    3.12 +command-line tools to work with the underlying Java Virtual Machine,
    3.13 +the Scala toplevel and compiler.  Note that Isabelle/jEdit
    3.14 +(\secref{sec:tool-tty}) provides a Scala Console for interactive
    3.15 +experimentation within the running application. *}
    3.16 +
    3.17 +
    3.18 +section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *}
    3.19 +
    3.20 +text {* The Isabelle @{tool_def java} utility is a direct wrapper for
    3.21 +  the Java Runtime Environment, within the regular Isabelle settings
    3.22 +  environment (\secref{sec:settings}).  The command line arguments are
    3.23 +  that of the underlying Java version.  It is run in @{verbatim
    3.24 +  "-server"} mode if possible, to improve performance (at the cost of
    3.25 +  extra startup time).
    3.26 +
    3.27 +  The @{verbatim java} executable is the one within @{setting
    3.28 +  ISABELLE_JDK_HOME}, according to the standard directory layout for
    3.29 +  official JDK distributions.  The class loader is augmented such that
    3.30 +  the name space of @{verbatim "Isabelle/Pure.jar"} is available,
    3.31 +  which is the main Isabelle/Scala module.
    3.32 +
    3.33 +  For example, the following command-line invokes the main method of
    3.34 +  class @{verbatim isabelle.GUI_Setup}, which opens a windows with
    3.35 +  some diagnostic information about the Isabelle environment:
    3.36 +\begin{alltt}
    3.37 +  isabelle java isabelle.GUI_Setup
    3.38 +\end{alltt}
    3.39 +*}
    3.40 +
    3.41 +
    3.42 +section {* Scala toplevel \label{sec:tool-scala} *}
    3.43 +
    3.44 +text {* The Isabelle @{tool_def scala} utility is a direct wrapper for
    3.45 +  the Scala toplevel; see also @{tool java} above.  The command line
    3.46 +  arguments are that of the underlying Scala version.
    3.47 +
    3.48 +  This allows to interact with Isabelle/Scala in TTY mode like this:
    3.49 +\begin{alltt}
    3.50 +  isabelle scala
    3.51 +  scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
    3.52 +  scala> isabelle.Isabelle_System.find_logics()
    3.53 +\end{alltt}
    3.54 +*}
    3.55 +
    3.56 +
    3.57 +section {* Scala compiler \label{sec:tool-scalac} *}
    3.58 +
    3.59 +text {* The Isabelle @{tool_def scalac} utility is a direct wrapper
    3.60 +  for the Scala compiler; see also @{tool scala} above.  The command
    3.61 +  line arguments are that of the underlying Scala version.
    3.62 +
    3.63 +  This allows to compile further Scala modules, depending on existing
    3.64 +  Isabelle/Scala functionality.  The resulting class or jar files can
    3.65 +  be added to the @{setting CLASSPATH} via the @{verbatim classpath}
    3.66 +  Bash function that is provided by the Isabelle process environment.
    3.67 +  Thus add-on components can register themselves in a modular manner,
    3.68 +  see also \secref{sec:components}.
    3.69 +
    3.70 +  Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
    3.71 +  adding plugin components, which needs special attention since
    3.72 +  it overrides the standard Java class loader.  *}
    3.73 +
    3.74 +end
     4.1 --- a/doc-src/System/Thy/document/Interfaces.tex	Sat Apr 28 17:05:31 2012 +0200
     4.2 +++ b/doc-src/System/Thy/document/Interfaces.tex	Sat Apr 28 17:50:42 2012 +0200
     4.3 @@ -94,7 +94,7 @@
     4.4  \end{isamarkuptext}%
     4.5  \isamarkuptrue%
     4.6  %
     4.7 -\isamarkupsection{Isabelle/jEdit Prover IDE%
     4.8 +\isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}%
     4.9  }
    4.10  \isamarkuptrue%
    4.11  %
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/System/Thy/document/Scala.tex	Sat Apr 28 17:50:42 2012 +0200
     5.3 @@ -0,0 +1,118 @@
     5.4 +%
     5.5 +\begin{isabellebody}%
     5.6 +\def\isabellecontext{Scala}%
     5.7 +%
     5.8 +\isadelimtheory
     5.9 +%
    5.10 +\endisadelimtheory
    5.11 +%
    5.12 +\isatagtheory
    5.13 +\isacommand{theory}\isamarkupfalse%
    5.14 +\ Scala\isanewline
    5.15 +\isakeyword{imports}\ Base\isanewline
    5.16 +\isakeyword{begin}%
    5.17 +\endisatagtheory
    5.18 +{\isafoldtheory}%
    5.19 +%
    5.20 +\isadelimtheory
    5.21 +%
    5.22 +\endisadelimtheory
    5.23 +%
    5.24 +\isamarkupchapter{Isabelle/Scala development tools%
    5.25 +}
    5.26 +\isamarkuptrue%
    5.27 +%
    5.28 +\begin{isamarkuptext}%
    5.29 +Isabelle/ML and Isabelle/Scala are the two main language
    5.30 +environments for Isabelle tool implementations.  There are some basic
    5.31 +command-line tools to work with the underlying Java Virtual Machine,
    5.32 +the Scala toplevel and compiler.  Note that Isabelle/jEdit
    5.33 +(\secref{sec:tool-tty}) provides a Scala Console for interactive
    5.34 +experimentation within the running application.%
    5.35 +\end{isamarkuptext}%
    5.36 +\isamarkuptrue%
    5.37 +%
    5.38 +\isamarkupsection{Java Runtime Environment within Isabelle \label{sec:tool-java}%
    5.39 +}
    5.40 +\isamarkuptrue%
    5.41 +%
    5.42 +\begin{isamarkuptext}%
    5.43 +The Isabelle \indexdef{}{tool}{java}\hypertarget{tool.java}{\hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}}} utility is a direct wrapper for
    5.44 +  the Java Runtime Environment, within the regular Isabelle settings
    5.45 +  environment (\secref{sec:settings}).  The command line arguments are
    5.46 +  that of the underlying Java version.  It is run in \verb|-server| mode if possible, to improve performance (at the cost of
    5.47 +  extra startup time).
    5.48 +
    5.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
    5.50 +  official JDK distributions.  The class loader is augmented such that
    5.51 +  the name space of \verb|Isabelle/Pure.jar| is available,
    5.52 +  which is the main Isabelle/Scala module.
    5.53 +
    5.54 +  For example, the following command-line invokes the main method of
    5.55 +  class \verb|isabelle.GUI_Setup|, which opens a windows with
    5.56 +  some diagnostic information about the Isabelle environment:
    5.57 +\begin{alltt}
    5.58 +  isabelle java isabelle.GUI_Setup
    5.59 +\end{alltt}%
    5.60 +\end{isamarkuptext}%
    5.61 +\isamarkuptrue%
    5.62 +%
    5.63 +\isamarkupsection{Scala toplevel \label{sec:tool-scala}%
    5.64 +}
    5.65 +\isamarkuptrue%
    5.66 +%
    5.67 +\begin{isamarkuptext}%
    5.68 +The Isabelle \indexdef{}{tool}{scala}\hypertarget{tool.scala}{\hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}}} utility is a direct wrapper for
    5.69 +  the Scala toplevel; see also \hyperlink{tool.java}{\mbox{\isa{\isatt{java}}}} above.  The command line
    5.70 +  arguments are that of the underlying Scala version.
    5.71 +
    5.72 +  This allows to interact with Isabelle/Scala in TTY mode like this:
    5.73 +\begin{alltt}
    5.74 +  isabelle scala
    5.75 +  scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
    5.76 +  scala> isabelle.Isabelle_System.find_logics()
    5.77 +\end{alltt}%
    5.78 +\end{isamarkuptext}%
    5.79 +\isamarkuptrue%
    5.80 +%
    5.81 +\isamarkupsection{Scala compiler \label{sec:tool-scalac}%
    5.82 +}
    5.83 +\isamarkuptrue%
    5.84 +%
    5.85 +\begin{isamarkuptext}%
    5.86 +The Isabelle \indexdef{}{tool}{scalac}\hypertarget{tool.scalac}{\hyperlink{tool.scalac}{\mbox{\isa{\isatt{scalac}}}}} utility is a direct wrapper
    5.87 +  for the Scala compiler; see also \hyperlink{tool.scala}{\mbox{\isa{\isatt{scala}}}} above.  The command
    5.88 +  line arguments are that of the underlying Scala version.
    5.89 +
    5.90 +  This allows to compile further Scala modules, depending on existing
    5.91 +  Isabelle/Scala functionality.  The resulting class or jar files can
    5.92 +  be added to the \hyperlink{setting.CLASSPATH}{\mbox{\isa{\isatt{CLASSPATH}}}} via the \verb|classpath|
    5.93 +  Bash function that is provided by the Isabelle process environment.
    5.94 +  Thus add-on components can register themselves in a modular manner,
    5.95 +  see also \secref{sec:components}.
    5.96 +
    5.97 +  Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
    5.98 +  adding plugin components, which needs special attention since
    5.99 +  it overrides the standard Java class loader.%
   5.100 +\end{isamarkuptext}%
   5.101 +\isamarkuptrue%
   5.102 +%
   5.103 +\isadelimtheory
   5.104 +%
   5.105 +\endisadelimtheory
   5.106 +%
   5.107 +\isatagtheory
   5.108 +\isacommand{end}\isamarkupfalse%
   5.109 +%
   5.110 +\endisatagtheory
   5.111 +{\isafoldtheory}%
   5.112 +%
   5.113 +\isadelimtheory
   5.114 +%
   5.115 +\endisadelimtheory
   5.116 +\isanewline
   5.117 +\end{isabellebody}%
   5.118 +%%% Local Variables:
   5.119 +%%% mode: latex
   5.120 +%%% TeX-master: "root"
   5.121 +%%% End:
     6.1 --- a/doc-src/System/system.tex	Sat Apr 28 17:05:31 2012 +0200
     6.2 +++ b/doc-src/System/system.tex	Sat Apr 28 17:50:42 2012 +0200
     6.3 @@ -31,6 +31,7 @@
     6.4  \input{Thy/document/Basics.tex}
     6.5  \input{Thy/document/Interfaces.tex}
     6.6  \input{Thy/document/Presentation.tex}
     6.7 +\input{Thy/document/Scala.tex}
     6.8  \input{Thy/document/Misc.tex}
     6.9  
    6.10  \begingroup
     7.1 --- a/doc-src/antiquote_setup.ML	Sat Apr 28 17:05:31 2012 +0200
     7.2 +++ b/doc-src/antiquote_setup.ML	Sat Apr 28 17:50:42 2012 +0200
     7.3 @@ -149,7 +149,8 @@
     7.4    in defined thy o intern thy end;
     7.5  
     7.6  fun check_tool name =
     7.7 -  File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
     7.8 +  let val tool_dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"]
     7.9 +  in exists (fn dir => File.exists (Path.append dir (Path.basic name))) tool_dirs end;
    7.10  
    7.11  val arg = enclose "{" "}" o clean_string;
    7.12