wenzelm@61656: (*:maxLineLen=78:*)
wenzelm@61575: 
wenzelm@47825: theory Scala
wenzelm@47825: imports Base
wenzelm@47825: begin
wenzelm@47825: 
wenzelm@58618: chapter \<open>Isabelle/Scala development tools\<close>
wenzelm@47825: 
wenzelm@61575: text \<open>
wenzelm@61575:   Isabelle/ML and Isabelle/Scala are the two main language environments for
wenzelm@61575:   Isabelle tool implementations. There are some basic command-line tools to
wenzelm@61575:   work with the underlying Java Virtual Machine, the Scala toplevel and
wenzelm@61575:   compiler. Note that Isabelle/jEdit @{cite "isabelle-jedit"} provides a Scala
wenzelm@61575:   Console for interactive experimentation within the running application.
wenzelm@61575: \<close>
wenzelm@47825: 
wenzelm@47825: 
wenzelm@58618: section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
wenzelm@47825: 
wenzelm@61575: text \<open>
wenzelm@61575:   The @{tool_def java} tool is a direct wrapper for the Java Runtime
wenzelm@61575:   Environment, within the regular Isabelle settings environment
wenzelm@61575:   (\secref{sec:settings}). The command line arguments are that of the
wenzelm@61575:   underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode if possible, to
wenzelm@61575:   improve performance (at the cost of extra startup time).
wenzelm@47825: 
wenzelm@61575:   The \<^verbatim>\<open>java\<close> executable is the one within @{setting ISABELLE_JDK_HOME},
wenzelm@61575:   according to the standard directory layout for official JDK distributions.
wenzelm@61575:   The class loader is augmented such that the name space of
wenzelm@61575:   \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module.
wenzelm@47825: 
wenzelm@61575:   For example, the following command-line invokes the main method of class
wenzelm@61575:   \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with some diagnostic
wenzelm@61575:   information about the Isabelle environment:
wenzelm@61407:   @{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
wenzelm@58618: \<close>
wenzelm@47825: 
wenzelm@47825: 
wenzelm@58618: section \<open>Scala toplevel \label{sec:tool-scala}\<close>
wenzelm@47825: 
wenzelm@61575: text \<open>
wenzelm@61575:   The @{tool_def scala} tool is a direct wrapper for the Scala toplevel; see
wenzelm@61575:   also @{tool java} above. The command line arguments are that of the
wenzelm@61575:   underlying Scala version.
wenzelm@47825: 
wenzelm@47825:   This allows to interact with Isabelle/Scala in TTY mode like this:
wenzelm@61407:   @{verbatim [display]
wenzelm@61407: \<open>isabelle scala
wenzelm@61407: scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
wenzelm@61407: scala> val options = isabelle.Options.init()
wenzelm@61407: scala> options.bool("browser_info")
wenzelm@61407: scala> options.string("document")\<close>}
wenzelm@58618: \<close>
wenzelm@47825: 
wenzelm@47825: 
wenzelm@58618: section \<open>Scala compiler \label{sec:tool-scalac}\<close>
wenzelm@47825: 
wenzelm@61575: text \<open>
wenzelm@61575:   The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
wenzelm@61575:   also @{tool scala} above. The command line arguments are that of the
wenzelm@61575:   underlying Scala version.
wenzelm@47825: 
wenzelm@47825:   This allows to compile further Scala modules, depending on existing
wenzelm@61575:   Isabelle/Scala functionality. The resulting class or jar files can be added
wenzelm@61575:   to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash function that is provided
wenzelm@61575:   by the Isabelle process environment. Thus add-on components can register
wenzelm@61575:   themselves in a modular manner, see also \secref{sec:components}.
wenzelm@47825: 
wenzelm@61575:   Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding
wenzelm@61575:   plugin components, which needs special attention since it overrides the
wenzelm@61575:   standard Java class loader.
wenzelm@61575: \<close>
wenzelm@47825: 
wenzelm@52116: 
wenzelm@58618: section \<open>Scala script wrapper\<close>
wenzelm@52116: 
wenzelm@61575: text \<open>
wenzelm@61575:   The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
wenzelm@61575:   allows to run Isabelle/Scala source files stand-alone programs, by using a
wenzelm@62415:   suitable ``hash-bang'' line and executable file permissions. For example:
wenzelm@61407:   @{verbatim [display]
wenzelm@61407: \<open>#!/usr/bin/env isabelle_scala_script
wenzelm@52116: 
wenzelm@52116: val options = isabelle.Options.init()
wenzelm@52116: Console.println("browser_info = " + options.bool("browser_info"))
wenzelm@61407: Console.println("document = " + options.string("document"))\<close>}
wenzelm@52116: 
wenzelm@62415:   This assumes that the executable may be found via the @{setting PATH} from
wenzelm@62415:   the process environment: this is the case when Isabelle settings are active,
wenzelm@62415:   e.g.\ in the context of the main Isabelle tool wrapper
wenzelm@63680:   \secref{sec:isabelle-tool}. Alternatively, the full
wenzelm@63680:   \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
wenzelm@62415:   form.
wenzelm@61575: \<close>
wenzelm@52116: 
wenzelm@47825: end