diff -r e717f152d2a8 -r f18f6e51e901 src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy Wed Nov 04 19:52:38 2015 +0100 +++ b/src/Doc/System/Scala.thy Wed Nov 04 20:18:46 2015 +0100 @@ -1,43 +1,47 @@ +(*:wrap=hard:maxLineLen=78:*) + 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 -@{cite "isabelle-jedit"} provides a Scala Console for interactive -experimentation within the running application.\ +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 @{cite "isabelle-jedit"} provides a Scala + Console for interactive experimentation within the running application. +\ section \Java Runtime Environment within Isabelle \label{sec:tool-java}\ -text \The @{tool_def java} tool 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). +text \ + The @{tool_def java} tool 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. + 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: + 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: @{verbatim [display] \isabelle java isabelle.GUI_Setup\} \ section \Scala toplevel \label{sec:tool-scala}\ -text \The @{tool_def scala} tool is a direct wrapper for the Scala - toplevel; see also @{tool java} above. The command line arguments - are that of the underlying Scala version. +text \ + The @{tool_def scala} tool 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: @{verbatim [display] @@ -51,32 +55,33 @@ section \Scala compiler \label{sec:tool-scalac}\ -text \The @{tool_def scalac} tool is a direct wrapper for the Scala - compiler; see also @{tool scala} above. The command line arguments - are that of the underlying Scala version. +text \ + The @{tool_def scalac} tool 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 Java classpath using 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}. + Isabelle/Scala functionality. The resulting class or jar files can be added + to the Java classpath using 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 @{cite "isabelle-jedit"} has its own mechanisms for - adding plugin components, which needs special attention since - it overrides the standard Java class loader.\ + Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding + plugin components, which needs special attention since it overrides the + standard Java class loader. +\ section \Scala script wrapper\ -text \The executable @{executable - "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run - Isabelle/Scala source files stand-alone programs, by using a +text \ + The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"} + allows to run Isabelle/Scala source files stand-alone programs, by using a suitable ``hash-bang'' line and executable file permissions. - The subsequent example assumes that the main Isabelle binaries have - been installed in some directory that is included in @{setting PATH} - (see also @{tool "install"}): + The subsequent example assumes that the main Isabelle binaries have been + installed in some directory that is included in @{setting PATH} (see also + @{tool "install"}): @{verbatim [display] \#!/usr/bin/env isabelle_scala_script @@ -84,8 +89,8 @@ Console.println("browser_info = " + options.bool("browser_info")) Console.println("document = " + options.string("document"))\} - Alternatively the full @{file - "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in - expanded form.\ + Alternatively the full @{file "$ISABELLE_HOME/bin/isabelle_scala_script"} + may be specified in expanded form. +\ end