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