src/Doc/System/Scala.thy
author haftmann
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06)
changeset 64990 c6a7de505796
parent 63680 6e1e8b5abbfa
permissions -rw-r--r--
more explicit errors in pathological cases
     1 (*:maxLineLen=78:*)
     2 
     3 theory Scala
     4 imports Base
     5 begin
     6 
     7 chapter \<open>Isabelle/Scala development tools\<close>
     8 
     9 text \<open>
    10   Isabelle/ML and Isabelle/Scala are the two main language environments for
    11   Isabelle tool implementations. There are some basic command-line tools to
    12   work with the underlying Java Virtual Machine, the Scala toplevel and
    13   compiler. Note that Isabelle/jEdit @{cite "isabelle-jedit"} provides a Scala
    14   Console for interactive experimentation within the running application.
    15 \<close>
    16 
    17 
    18 section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
    19 
    20 text \<open>
    21   The @{tool_def java} tool is a direct wrapper for the Java Runtime
    22   Environment, within the regular Isabelle settings environment
    23   (\secref{sec:settings}). The command line arguments are that of the
    24   underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode if possible, to
    25   improve performance (at the cost of extra startup time).
    26 
    27   The \<^verbatim>\<open>java\<close> executable is the one within @{setting ISABELLE_JDK_HOME},
    28   according to the standard directory layout for official JDK distributions.
    29   The class loader is augmented such that the name space of
    30   \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module.
    31 
    32   For example, the following command-line invokes the main method of class
    33   \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with some diagnostic
    34   information about the Isabelle environment:
    35   @{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
    36 \<close>
    37 
    38 
    39 section \<open>Scala toplevel \label{sec:tool-scala}\<close>
    40 
    41 text \<open>
    42   The @{tool_def scala} tool is a direct wrapper for the Scala toplevel; see
    43   also @{tool java} above. The command line arguments are that of the
    44   underlying Scala version.
    45 
    46   This allows to interact with Isabelle/Scala in TTY mode like this:
    47   @{verbatim [display]
    48 \<open>isabelle scala
    49 scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
    50 scala> val options = isabelle.Options.init()
    51 scala> options.bool("browser_info")
    52 scala> options.string("document")\<close>}
    53 \<close>
    54 
    55 
    56 section \<open>Scala compiler \label{sec:tool-scalac}\<close>
    57 
    58 text \<open>
    59   The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
    60   also @{tool scala} above. The command line arguments are that of the
    61   underlying Scala version.
    62 
    63   This allows to compile further Scala modules, depending on existing
    64   Isabelle/Scala functionality. The resulting class or jar files can be added
    65   to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash function that is provided
    66   by the Isabelle process environment. Thus add-on components can register
    67   themselves in a modular manner, see also \secref{sec:components}.
    68 
    69   Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding
    70   plugin components, which needs special attention since it overrides the
    71   standard Java class loader.
    72 \<close>
    73 
    74 
    75 section \<open>Scala script wrapper\<close>
    76 
    77 text \<open>
    78   The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
    79   allows to run Isabelle/Scala source files stand-alone programs, by using a
    80   suitable ``hash-bang'' line and executable file permissions. For example:
    81   @{verbatim [display]
    82 \<open>#!/usr/bin/env isabelle_scala_script
    83 
    84 val options = isabelle.Options.init()
    85 Console.println("browser_info = " + options.bool("browser_info"))
    86 Console.println("document = " + options.string("document"))\<close>}
    87 
    88   This assumes that the executable may be found via the @{setting PATH} from
    89   the process environment: this is the case when Isabelle settings are active,
    90   e.g.\ in the context of the main Isabelle tool wrapper
    91   \secref{sec:isabelle-tool}. Alternatively, the full
    92   \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
    93   form.
    94 \<close>
    95 
    96 end