added "isabelle scala_project" to support e.g. IntelliJ IDEA;
(*:maxLineLen=78:*)
theory Scala
imports Base
begin
chapter \<open>Isabelle/Scala development tools\<close>
text \<open>
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.
\<close>
section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
text \<open>
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>\<open>-server\<close> mode if possible, to
improve performance (at the cost of extra startup time).
The \<^verbatim>\<open>java\<close> 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>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module.
For example, the following command-line invokes the main method of class
\<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with some diagnostic
information about the Isabelle environment:
@{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
\<close>
section \<open>Scala toplevel \label{sec:tool-scala}\<close>
text \<open>
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]
\<open>isabelle scala
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
scala> val options = isabelle.Options.init()
scala> options.bool("browser_info")
scala> options.string("document")\<close>}
\<close>
section \<open>Scala compiler \label{sec:tool-scalac}\<close>
text \<open>
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>\<open>classpath\<close> 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.
\<close>
section \<open>Scala script wrapper\<close>
text \<open>
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. For example:
@{verbatim [display]
\<open>#!/usr/bin/env isabelle_scala_script
val options = isabelle.Options.init()
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))\<close>}
This assumes that the executable may be found via the @{setting PATH} from
the process environment: this is the case when Isabelle settings are active,
e.g.\ in the context of the main Isabelle tool wrapper
\secref{sec:isabelle-tool}. Alternatively, the full
\<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
form.
\<close>
section \<open>Project setup for common Scala IDEs\<close>
text \<open>
The @{tool_def scala_project} tool creates a Gradle project configuration
for Isabelle/Scala/jEdit:
@{verbatim [display]
\<open>Usage: isabelle scala_project [OPTIONS] PROJECT_DIR
Options are:
-l make symlinks to original scala files
Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
such as IntelliJ IDEA.\<close>}
The generated project configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close>,
but the main purpose is to import it into common Scala IDEs, such as
IntelliJ IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore
the sources with static analysis and other hints in real-time.
The specified project directory must not exist yet. The generated files
refer to physical file locations, using the path notation of the underlying
OS platform. Thus the project needs to be recreated whenever the Isabelle
installation is changed or moved.
\<^medskip> By default, Scala sources are \<^emph>\<open>copied\<close> from the Isabelle distribution and
editing them within the IDE has no permanent effect.
Alternatively, option \<^verbatim>\<open>-l\<close> may be used to produce symlinks to the original
files: this allows to develop Isabelle/Scala/jEdit within an external Scala
IDE. Note that building the result always requires \<^verbatim>\<open>isabelle jedit -b\<close> on
the command-line.
\<close>
end