documentation for Isabelle/Scala tools;
authorwenzelm
Sun Nov 20 15:53:07 2016 +0100 (2016-11-20)
changeset 6450980aaa4ff7fed
parent 64508 874555896035
child 64510 488cb71eeb83
documentation for Isabelle/Scala tools;
tuned;
src/Doc/System/Environment.thy
     1.1 --- a/src/Doc/System/Environment.thy	Sat Nov 19 20:10:32 2016 +0100
     1.2 +++ b/src/Doc/System/Environment.thy	Sun Nov 20 15:53:07 2016 +0100
     1.3 @@ -214,8 +214,8 @@
     1.4  
     1.5      \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
     1.6      bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
     1.7 -    usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
     1.8 -    component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
     1.9 +    usual, the content is interpreted as a GNU bash script. It may refer to
    1.10 +    the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
    1.11  
    1.12      For example, the following setting allows to refer to files within the
    1.13      component later on, without having to hardwire absolute paths:
    1.14 @@ -260,9 +260,12 @@
    1.15  
    1.16  text \<open>
    1.17    The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
    1.18 -  Isabelle related utilities, user interfaces etc. Such tools automatically
    1.19 -  benefit from the settings mechanism. All Isabelle command-line tools are
    1.20 -  invoked via a common wrapper --- @{executable_ref isabelle}:
    1.21 +  Isabelle-related utilities, user interfaces, add-on applications etc. Such
    1.22 +  tools automatically benefit from the settings mechanism
    1.23 +  (\secref{sec:settings}). Moreover, this is the standard way to invoke
    1.24 +  Isabelle/Scala functionality as a separate operating-system process.
    1.25 +  Isabelle command-line tools are run uniformly via a common wrapper ---
    1.26 +  @{executable_ref isabelle}:
    1.27    @{verbatim [display]
    1.28  \<open>Usage: isabelle TOOL [ARGS ...]
    1.29  
    1.30 @@ -271,12 +274,32 @@
    1.31  Available tools:
    1.32    ...\<close>}
    1.33  
    1.34 -  In principle, Isabelle tools are ordinary executable scripts that are run
    1.35 -  within the Isabelle settings environment, see \secref{sec:settings}. The set
    1.36 -  of available tools is collected by @{executable isabelle} from the
    1.37 -  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
    1.38 -  call the scripts directly from the shell. Neither should you add the tool
    1.39 -  directories to your shell's search path!
    1.40 +  Tools may be implemented in Isabelle/Scala or as stand-alone executables
    1.41 +  (usually as GNU bash scripts). In the invocation of ``@{executable
    1.42 +  isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the
    1.43 +  given order).
    1.44 +
    1.45 +    \<^enum> An external tool found on the directories listed in the @{setting
    1.46 +    ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
    1.47 +    notation).
    1.48 +
    1.49 +      \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define
    1.50 +      some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala
    1.51 +      compiler is invoked on the spot (which may take some time), and the body
    1.52 +      function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.
    1.53 +
    1.54 +      \<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as
    1.55 +      stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
    1.56 +      array.
    1.57 +
    1.58 +    \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
    1.59 +    within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
    1.60 +    entry-point for high-end tools implemented in Isabelle/Scala --- compiled
    1.61 +    once when the Isabelle distribution is built. These tools are provided by
    1.62 +    Isabelle/Pure and cannot be augmented in user-space.
    1.63 +
    1.64 +  There are also some administrative tools that are available from a bare
    1.65 +  repository clone of Isabelle, but not in regular distributions.
    1.66  \<close>
    1.67  
    1.68  
    1.69 @@ -346,7 +369,7 @@
    1.70    loader within ML:
    1.71    @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
    1.72  
    1.73 -  Observe the delicate quoting rules for the Bash shell vs.\ ML. The
    1.74 +  Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
    1.75    Isabelle/ML and Scala libraries provide functions for that, but here we need
    1.76    to do it manually.
    1.77  \<close>