wenzelm@47825: theory Scala wenzelm@47825: imports Base wenzelm@47825: begin wenzelm@47825: wenzelm@47825: chapter {* Isabelle/Scala development tools *} wenzelm@47825: wenzelm@47825: text {* Isabelle/ML and Isabelle/Scala are the two main language wenzelm@47825: environments for Isabelle tool implementations. There are some basic wenzelm@47825: command-line tools to work with the underlying Java Virtual Machine, wenzelm@47825: the Scala toplevel and compiler. Note that Isabelle/jEdit wenzelm@47825: (\secref{sec:tool-tty}) provides a Scala Console for interactive wenzelm@47825: experimentation within the running application. *} wenzelm@47825: wenzelm@47825: wenzelm@47825: section {* Java Runtime Environment within Isabelle \label{sec:tool-java} *} wenzelm@47825: wenzelm@48602: text {* The @{tool_def java} tool is a direct wrapper for the Java wenzelm@48602: Runtime Environment, within the regular Isabelle settings wenzelm@47825: environment (\secref{sec:settings}). The command line arguments are wenzelm@47825: that of the underlying Java version. It is run in @{verbatim wenzelm@47825: "-server"} mode if possible, to improve performance (at the cost of wenzelm@47825: extra startup time). wenzelm@47825: wenzelm@47825: The @{verbatim java} executable is the one within @{setting wenzelm@47825: ISABELLE_JDK_HOME}, according to the standard directory layout for wenzelm@47825: official JDK distributions. The class loader is augmented such that wenzelm@47825: the name space of @{verbatim "Isabelle/Pure.jar"} is available, wenzelm@47825: which is the main Isabelle/Scala module. wenzelm@47825: wenzelm@47825: For example, the following command-line invokes the main method of wenzelm@47825: class @{verbatim isabelle.GUI_Setup}, which opens a windows with wenzelm@47825: some diagnostic information about the Isabelle environment: wenzelm@47825: \begin{alltt} wenzelm@47825: isabelle java isabelle.GUI_Setup wenzelm@47825: \end{alltt} wenzelm@47825: *} wenzelm@47825: wenzelm@47825: wenzelm@47825: section {* Scala toplevel \label{sec:tool-scala} *} wenzelm@47825: wenzelm@48602: text {* The @{tool_def scala} tool is a direct wrapper for the Scala wenzelm@48602: toplevel; see also @{tool java} above. The command line arguments wenzelm@48602: are that of the underlying Scala version. wenzelm@47825: wenzelm@47825: This allows to interact with Isabelle/Scala in TTY mode like this: wenzelm@47825: \begin{alltt} wenzelm@47825: isabelle scala wenzelm@47825: scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME") wenzelm@48815: scala> val options = isabelle.Options.init() wenzelm@48815: scala> options.bool("browser_info") wenzelm@47825: \end{alltt} wenzelm@47825: *} wenzelm@47825: wenzelm@47825: wenzelm@47825: section {* Scala compiler \label{sec:tool-scalac} *} wenzelm@47825: wenzelm@48602: text {* The @{tool_def scalac} tool is a direct wrapper for the Scala wenzelm@48602: compiler; see also @{tool scala} above. The command line arguments wenzelm@48602: are that of the underlying Scala version. wenzelm@47825: wenzelm@47825: This allows to compile further Scala modules, depending on existing wenzelm@47825: Isabelle/Scala functionality. The resulting class or jar files can wenzelm@47825: be added to the @{setting CLASSPATH} via the @{verbatim classpath} wenzelm@47825: Bash function that is provided by the Isabelle process environment. wenzelm@47825: Thus add-on components can register themselves in a modular manner, wenzelm@47825: see also \secref{sec:components}. wenzelm@47825: wenzelm@47825: Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for wenzelm@47825: adding plugin components, which needs special attention since wenzelm@47825: it overrides the standard Java class loader. *} wenzelm@47825: wenzelm@47825: end