isabelle_process is superseded by "isabelle process" tool;
authorwenzelm
Thu Mar 10 12:11:50 2016 +0100 (2016-03-10)
changeset 62588cd266473b81b
parent 62587 e31bf8ed5397
child 62589 b5783412bfed
isabelle_process is superseded by "isabelle process" tool;
tuned tool usage;
misc updates and tuning of "system" manual;
NEWS
bin/isabelle_process
lib/Tools/console
lib/Tools/install
lib/Tools/process
lib/scripts/getsettings
src/Doc/System/Basics.thy
src/Doc/System/Misc.thy
src/Doc/System/Presentation.thy
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
src/HOL/Mutabelle/lib/Tools/mutabelle
src/HOL/TPTP/CASC/ReadMe
src/HOL/TPTP/lib/Tools/tptp_graph
src/HOL/TPTP/lib/Tools/tptp_isabelle
src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
src/HOL/TPTP/lib/Tools/tptp_nitpick
src/HOL/TPTP/lib/Tools/tptp_refute
src/HOL/TPTP/lib/Tools/tptp_sledgehammer
src/HOL/TPTP/lib/Tools/tptp_translate
src/Pure/Tools/ml_console.scala
src/Pure/Tools/ml_process.scala
src/Tools/Code/code_ml.ML
     1.1 --- a/NEWS	Thu Mar 10 12:11:23 2016 +0100
     1.2 +++ b/NEWS	Thu Mar 10 12:11:50 2016 +0100
     1.3 @@ -218,6 +218,29 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* SML/NJ and old versions of Poly/ML are no longer supported.
     1.8 +
     1.9 +* The executable "isabelle_process" has been discontinued. Tools and
    1.10 +prover front-ends should use ML_Process or Isabelle_Process in
    1.11 +Isabelle/Scala. Command-line usage works via "isabelle process" or
    1.12 +"isabelle console". INCOMPATIBILITY.
    1.13 +
    1.14 +* The Isabelle system environment always ensures that the main
    1.15 +executables are found within the shell search $PATH: "isabelle" and
    1.16 +"isabelle_scala_script".
    1.17 +
    1.18 +* New command-line tool "isabelle process" supports ML evaluation of
    1.19 +literal expressions (option -e) or files (option -f) in the context of a
    1.20 +given heap image. Errors lead to premature exit of the ML process with
    1.21 +return code 1.
    1.22 +
    1.23 +* Command-line tool "isabelle console" provides option -r to help to
    1.24 +bootstrapping Isabelle/Pure interactively.
    1.25 +
    1.26 +* Command-line tool "isabelle yxml" has been discontinued.
    1.27 +INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
    1.28 +Isabelle/ML or Isabelle/Scala.
    1.29 +
    1.30  * File.bash_string, File.bash_path etc. represent Isabelle/ML and
    1.31  Isabelle/Scala strings authentically within GNU bash. This is useful to
    1.32  produce robust shell scripts under program control, without worrying
    1.33 @@ -226,27 +249,6 @@
    1.34  less versatile) operations File.shell_quote, File.shell_path etc. have
    1.35  been discontinued.
    1.36  
    1.37 -* The Isabelle system environment always ensures that the main
    1.38 -executables are found within the PATH: isabelle, isabelle_process,
    1.39 -isabelle_scala_script.
    1.40 -
    1.41 -* Command-line tool "isabelle_process" no longer supports writable heap
    1.42 -images. INCOMPATIBILITY in exotic situations where "isabelle build"
    1.43 -cannot be used: the structure ML_Heap provides operations to save the ML
    1.44 -heap under program control.
    1.45 -
    1.46 -* Command-line tool "isabelle_process" supports ML evaluation of literal
    1.47 -expressions (option -e) or files (option -f). Errors lead to premature
    1.48 -exit of the ML process with return code 1.
    1.49 -
    1.50 -* Command-line tool "isabelle console -r" helps to bootstrap
    1.51 -Isabelle/Pure interactively.
    1.52 -
    1.53 -* The somewhat pointless command-line tool "isabelle yxml" has been
    1.54 -discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
    1.55 -"YXML" in Isabelle/ML or Isabelle/Scala.
    1.56 -
    1.57 -* SML/NJ and old versions of Poly/ML are no longer supported.
    1.58  
    1.59  
    1.60  New in Isabelle2016 (February 2016)
     2.1 --- a/bin/isabelle_process	Thu Mar 10 12:11:23 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,18 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Makarius
     2.7 -#
     2.8 -# Isabelle process startup script.
     2.9 -
    2.10 -if [ -L "$0" ]; then
    2.11 -  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
    2.12 -  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
    2.13 -fi
    2.14 -
    2.15 -ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
    2.16 -source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
    2.17 -
    2.18 -
    2.19 -isabelle_admin_build jars || exit $?
    2.20 -
    2.21 -"$ISABELLE_TOOL" java isabelle.ML_Process "$@"
     3.1 --- a/lib/Tools/console	Thu Mar 10 12:11:23 2016 +0100
     3.2 +++ b/lib/Tools/console	Thu Mar 10 12:11:50 2016 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4  #
     3.5  # Author: Makarius
     3.6  #
     3.7 -# DESCRIPTION: run Isabelle process with raw ML console and line editor
     3.8 +# DESCRIPTION: raw ML process (interactive mode)
     3.9  
    3.10  isabelle_admin_build jars || exit $?
    3.11  
     4.1 --- a/lib/Tools/install	Thu Mar 10 12:11:23 2016 +0100
     4.2 +++ b/lib/Tools/install	Thu Mar 10 12:11:50 2016 +0100
     4.3 @@ -63,7 +63,7 @@
     4.4  
     4.5  mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
     4.6  
     4.7 -for NAME in isabelle isabelle_process isabelle_scala_script
     4.8 +for NAME in isabelle isabelle_scala_script
     4.9  do
    4.10    BIN="$BINDIR/$NAME"
    4.11    DIST="$DISTDIR/bin/$NAME"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/lib/Tools/process	Thu Mar 10 12:11:50 2016 +0100
     5.3 @@ -0,0 +1,22 @@
     5.4 +#!/usr/bin/env bash
     5.5 +#
     5.6 +# Author: Makarius
     5.7 +#
     5.8 +# DESCRIPTION: raw ML process (batch mode)
     5.9 +
    5.10 +isabelle_admin_build jars || exit $?
    5.11 +
    5.12 +case "$ISABELLE_JAVA_PLATFORM" in
    5.13 +  x86-*)
    5.14 +    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
    5.15 +    ;;
    5.16 +  x86_64-*)
    5.17 +    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
    5.18 +    ;;
    5.19 +esac
    5.20 +
    5.21 +declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    5.22 +
    5.23 +mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
    5.24 +
    5.25 +"$ISABELLE_TOOL" java isabelle.ML_Process "$@"
     6.1 --- a/lib/scripts/getsettings	Thu Mar 10 12:11:23 2016 +0100
     6.2 +++ b/lib/scripts/getsettings	Thu Mar 10 12:11:50 2016 +0100
     6.3 @@ -55,7 +55,6 @@
     6.4  
     6.5  #main executables
     6.6  ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
     6.7 -ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
     6.8  ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script"
     6.9  PATH="$ISABELLE_HOME/bin:$PATH"
    6.10  
     7.1 --- a/src/Doc/System/Basics.thy	Thu Mar 10 12:11:23 2016 +0100
     7.2 +++ b/src/Doc/System/Basics.thy	Thu Mar 10 12:11:50 2016 +0100
     7.3 @@ -7,49 +7,24 @@
     7.4  chapter \<open>The Isabelle system environment\<close>
     7.5  
     7.6  text \<open>
     7.7 -  This manual describes Isabelle together with related tools and user
     7.8 -  interfaces as seen from a system oriented view. See also the \<^emph>\<open>Isabelle/Isar
     7.9 -  Reference Manual\<close> @{cite "isabelle-isar-ref"} for the actual Isabelle input
    7.10 -  language and related concepts, and \<^emph>\<open>The Isabelle/Isar Implementation
    7.11 -  Manual\<close> @{cite "isabelle-implementation"} for the main concepts of the
    7.12 -  underlying implementation in Isabelle/ML.
    7.13 -
    7.14 -  \<^medskip>
    7.15 -  The Isabelle system environment provides the following basic infrastructure
    7.16 -  to integrate tools smoothly.
    7.17 -
    7.18 -  \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process environment variables
    7.19 -  to all Isabelle executables (including tools and user interfaces).
    7.20 -
    7.21 -  \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
    7.22 -  logic sessions in batch mode. This is rarely required for regular users.
    7.23 -
    7.24 -  \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
    7.25 -  generic startup environment Isabelle related utilities, user interfaces etc.
    7.26 -  Such tools automatically benefit from the settings mechanism.
    7.27 +  This manual describes Isabelle together with related tools as seen from a
    7.28 +  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
    7.29 +  "isabelle-isar-ref"} for the actual Isabelle input language and related
    7.30 +  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
    7.31 +  "isabelle-implementation"} for the main concepts of the underlying
    7.32 +  implementation in Isabelle/ML.
    7.33  \<close>
    7.34  
    7.35  
    7.36  section \<open>Isabelle settings \label{sec:settings}\<close>
    7.37  
    7.38  text \<open>
    7.39 -  The Isabelle system heavily depends on the \<^emph>\<open>settings mechanism\<close>.
    7.40 -  Essentially, this is a statically scoped collection of environment
    7.41 +  Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
    7.42 +  process environment. This is a statically scoped collection of environment
    7.43    variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
    7.44    ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
    7.45 -  shell, though. Isabelle employs a somewhat more sophisticated scheme of
    7.46 -  \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for additional
    7.47 -  user-specific modifications. With all configuration variables in clearly
    7.48 -  defined places, this scheme is more maintainable and user-friendly than
    7.49 -  global shell environment variables.
    7.50 -
    7.51 -  In particular, we avoid the typical situation where prospective users of a
    7.52 -  software package are told to put several things into their shell startup
    7.53 -  scripts, before being able to actually run the program. Isabelle requires
    7.54 -  none such administrative chores of its end-users --- the executables can be
    7.55 -  invoked straight away. Occasionally, users would still want to put the
    7.56 -  @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but
    7.57 -  this is not required.
    7.58 +  shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
    7.59 +  explained below.
    7.60  \<close>
    7.61  
    7.62  
    7.63 @@ -101,9 +76,8 @@
    7.64    \<^medskip>
    7.65    A few variables are somewhat special:
    7.66  
    7.67 -    \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
    7.68 -    automatically to the absolute path names of the @{executable
    7.69 -    "isabelle_process"} and @{executable isabelle} executables, respectively.
    7.70 +    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
    7.71 +    name of the @{executable isabelle} executables.
    7.72  
    7.73      \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
    7.74      distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
    7.75 @@ -162,11 +136,10 @@
    7.76  
    7.77    @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
    7.78  
    7.79 -  \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] are
    7.80 -  automatically set to the full path names of the @{executable
    7.81 -  "isabelle_process"} and @{executable isabelle} executables, respectively.
    7.82 -  Thus other tools and scripts need not assume that the @{file
    7.83 -  "$ISABELLE_HOME/bin"} directory is on the current search path of the shell.
    7.84 +  \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
    7.85 +  of the @{executable isabelle} executable. Thus other tools and scripts need
    7.86 +  not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
    7.87 +  search path of the shell.
    7.88  
    7.89    \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
    7.90    Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
    7.91 @@ -228,8 +201,8 @@
    7.92    \<^verbatim>\<open>dvi\<close> files.
    7.93  
    7.94    \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
    7.95 -  running @{executable "isabelle_process"} derives an individual directory for
    7.96 -  temporary files.
    7.97 +  running Isabelle ML process derives an individual directory for temporary
    7.98 +  files.
    7.99  \<close>
   7.100  
   7.101  
   7.102 @@ -284,13 +257,52 @@
   7.103  \<close>
   7.104  
   7.105  
   7.106 -section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
   7.107 +section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
   7.108  
   7.109  text \<open>
   7.110 -  The @{executable_def "isabelle_process"} executable runs a bare-bone
   7.111 -  Isabelle logic session in batch mode:
   7.112 +  The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
   7.113 +  Isabelle related utilities, user interfaces etc. Such tools automatically
   7.114 +  benefit from the settings mechanism. All Isabelle command-line tools are
   7.115 +  invoked via a common wrapper --- @{executable_ref isabelle}:
   7.116    @{verbatim [display]
   7.117 -\<open>Usage: isabelle_process [OPTIONS] [HEAP]
   7.118 +\<open>Usage: isabelle TOOL [ARGS ...]
   7.119 +
   7.120 +  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   7.121 +
   7.122 +Available tools:
   7.123 +  ...\<close>}
   7.124 +
   7.125 +  In principle, Isabelle tools are ordinary executable scripts that are run
   7.126 +  within the Isabelle settings environment, see \secref{sec:settings}. The set
   7.127 +  of available tools is collected by @{executable isabelle} from the
   7.128 +  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
   7.129 +  call the scripts directly from the shell. Neither should you add the tool
   7.130 +  directories to your shell's search path!
   7.131 +\<close>
   7.132 +
   7.133 +
   7.134 +subsubsection \<open>Examples\<close>
   7.135 +
   7.136 +text \<open>
   7.137 +  Show the list of available documentation of the Isabelle distribution:
   7.138 +  @{verbatim [display] \<open>isabelle doc\<close>}
   7.139 +
   7.140 +  View a certain document as follows:
   7.141 +  @{verbatim [display] \<open>isabelle doc system\<close>}
   7.142 +
   7.143 +  Query the Isabelle settings environment:
   7.144 +  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
   7.145 +\<close>
   7.146 +
   7.147 +
   7.148 +section \<open>The raw Isabelle ML process\<close>
   7.149 +
   7.150 +subsection \<open>Batch mode \label{sec:tool-process}\<close>
   7.151 +
   7.152 +text \<open>
   7.153 +  The @{tool_def process} tool runs the raw ML process in batch mode:
   7.154 +  @{verbatim [display]
   7.155 +\<open>Usage: isabelle process [OPTIONS] [HEAP]
   7.156  
   7.157    Options are:
   7.158      -e ML_EXPR   evaluate ML expression on startup
   7.159 @@ -298,8 +310,10 @@
   7.160      -m MODE      add print mode for output
   7.161      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   7.162  
   7.163 -  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
   7.164 -  $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
   7.165 +  Run the raw Isabelle ML process in batch mode, using a given heap image.
   7.166 +
   7.167 +  If HEAP is a plain name (default ISABELLE_LOGIC), it is searched in
   7.168 +  ISABELLE_PATH; if it contains a slash, it is taken as literal file;
   7.169    if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
   7.170  
   7.171    Heap files without explicit directory specifications are looked up in the
   7.172 @@ -328,49 +342,60 @@
   7.173  \<close>
   7.174  
   7.175  
   7.176 -subsubsection \<open>Examples\<close>
   7.177 +subsubsection \<open>Example\<close>
   7.178  
   7.179  text \<open>
   7.180 -  In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close>
   7.181 -  theory value from the theory loader within ML (observe the delicate quoting
   7.182 -  rules for the Bash shell vs.\ ML):
   7.183 -  @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
   7.184 +  The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
   7.185 +  loader within ML:
   7.186 +  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
   7.187 +
   7.188 +  Observe the delicate quoting rules for the Bash shell vs.\ ML. The
   7.189 +  Isabelle/ML and Scala libraries provide functions for that, but here we need
   7.190 +  to do it manually.
   7.191  \<close>
   7.192  
   7.193  
   7.194 -section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
   7.195 +subsection \<open>Interactive mode\<close>
   7.196  
   7.197  text \<open>
   7.198 -  All Isabelle related tools and interfaces are called via a common wrapper
   7.199 -  --- @{executable isabelle}:
   7.200 +  The @{tool_def console} tool runs the raw ML process with interactive
   7.201 +  console and line editor:
   7.202    @{verbatim [display]
   7.203 -\<open>Usage: isabelle TOOL [ARGS ...]
   7.204 +\<open>Usage: isabelle console [OPTIONS]
   7.205  
   7.206 -  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   7.207 +  Options are:
   7.208 +    -d DIR       include session directory
   7.209 +    -l NAME      logic session name (default ISABELLE_LOGIC)
   7.210 +    -m MODE      add print mode for output
   7.211 +    -n           no build of session image on startup
   7.212 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   7.213 +    -r           logic session is RAW_ML_SYSTEM
   7.214 +    -s           system build mode for session image
   7.215  
   7.216 -Available tools:
   7.217 -  ...\<close>}
   7.218 +  Build a logic session image and run the raw Isabelle ML process
   7.219 +  in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
   7.220  
   7.221 -  In principle, Isabelle tools are ordinary executable scripts that are run
   7.222 -  within the Isabelle settings environment, see \secref{sec:settings}. The set
   7.223 -  of available tools is collected by @{executable isabelle} from the
   7.224 -  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
   7.225 -  call the scripts directly from the shell. Neither should you add the tool
   7.226 -  directories to your shell's search path!
   7.227 -\<close>
   7.228 +  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
   7.229 +  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
   7.230 +  abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
   7.231 +  Isabelle/Pure interactively.
   7.232  
   7.233 +  Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
   7.234 +  (\secref{sec:tool-build}).
   7.235 +
   7.236 +  Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
   7.237 +  (\secref{sec:tool-process}).
   7.238  
   7.239 -subsubsection \<open>Examples\<close>
   7.240 -
   7.241 -text \<open>
   7.242 -  Show the list of available documentation of the Isabelle distribution:
   7.243 -  @{verbatim [display] \<open>isabelle doc\<close>}
   7.244 +  \<^medskip>
   7.245 +  The Isabelle/ML process is run through the line editor that is specified via
   7.246 +  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
   7.247 +  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
   7.248 +  standard input/output.
   7.249  
   7.250 -  View a certain document as follows:
   7.251 -  @{verbatim [display] \<open>isabelle doc system\<close>}
   7.252 -
   7.253 -  Query the Isabelle settings environment:
   7.254 -  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
   7.255 +  The user is connected to the raw ML toplevel loop: this is neither
   7.256 +  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
   7.257 +  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
   7.258 +  use_thys}.
   7.259  \<close>
   7.260  
   7.261  
     8.1 --- a/src/Doc/System/Misc.thy	Thu Mar 10 12:11:23 2016 +0100
     8.2 +++ b/src/Doc/System/Misc.thy	Thu Mar 10 12:11:50 2016 +0100
     8.3 @@ -56,49 +56,6 @@
     8.4  \<close>
     8.5  
     8.6  
     8.7 -section \<open>Raw ML console\<close>
     8.8 -
     8.9 -text \<open>
    8.10 -  The @{tool_def console} tool runs the Isabelle process with raw ML console:
    8.11 -  @{verbatim [display]
    8.12 -\<open>Usage: isabelle console [OPTIONS]
    8.13 -
    8.14 -  Options are:
    8.15 -    -d DIR       include session directory
    8.16 -    -l NAME      logic session name (default ISABELLE_LOGIC)
    8.17 -    -m MODE      add print mode for output
    8.18 -    -n           no build of session image on startup
    8.19 -    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    8.20 -    -r           logic session is RAW_ML_SYSTEM
    8.21 -    -s           system build mode for session image
    8.22 -
    8.23 -  Run Isabelle process with raw ML console and line editor
    8.24 -  (default ISABELLE_LINE_EDITOR).\<close>}
    8.25 -
    8.26 -  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
    8.27 -  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that. Option \<^verbatim>\<open>-r\<close>
    8.28 -  abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
    8.29 -  Isabelle/Pure interactively.
    8.30 -
    8.31 -  Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
    8.32 -  (\secref{sec:tool-build}).
    8.33 -
    8.34 -  Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for the raw @{executable
    8.35 -  isabelle_process} (\secref{sec:isabelle-process}).
    8.36 -
    8.37 -  \<^medskip>
    8.38 -  The Isabelle/ML process is run through the line editor that is specified via
    8.39 -  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
    8.40 -  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
    8.41 -  standard input/output.
    8.42 -
    8.43 -  The user is connected to the raw ML toplevel loop: this is neither
    8.44 -  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
    8.45 -  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
    8.46 -  use_thys}.
    8.47 -\<close>
    8.48 -
    8.49 -
    8.50  section \<open>Displaying documents \label{sec:tool-display}\<close>
    8.51  
    8.52  text \<open>
    8.53 @@ -213,7 +170,7 @@
    8.54    determined by @{setting ISABELLE_HOME}.
    8.55  
    8.56    The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
    8.57 -  @{executable "isabelle_process"} and @{executable isabelle} should be
    8.58 +  @{executable "isabelle"} and @{executable isabelle_scala_script} should be
    8.59    placed, which is typically a directory in the shell's @{setting PATH}, such
    8.60    as \<^verbatim>\<open>$HOME/bin\<close>.
    8.61  
     9.1 --- a/src/Doc/System/Presentation.thy	Thu Mar 10 12:11:23 2016 +0100
     9.2 +++ b/src/Doc/System/Presentation.thy	Thu Mar 10 12:11:50 2016 +0100
     9.3 @@ -17,11 +17,10 @@
     9.4  
     9.5    The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
     9.6    for managing Isabelle sessions, including proper setup for presentation;
     9.7 -  @{tool build} takes care to have @{executable_ref "isabelle_process"} run
     9.8 -  any additional stages required for document preparation, notably the
     9.9 -  @{tool_ref document} and @{tool_ref latex}. The complete tool chain for
    9.10 -  managing batch-mode Isabelle sessions is illustrated in
    9.11 -  \figref{fig:session-tools}.
    9.12 +  @{tool build} tells the Isabelle process to run any additional stages
    9.13 +  required for document preparation, notably the @{tool_ref document} and
    9.14 +  @{tool_ref latex}. The complete tool chain for managing batch-mode Isabelle
    9.15 +  sessions is illustrated in \figref{fig:session-tools}.
    9.16  
    9.17    \begin{figure}[htbp]
    9.18    \begin{center}
    9.19 @@ -34,8 +33,7 @@
    9.20        @{tool_ref build} & invoked repeatedly by the user to keep
    9.21        session output up-to-date (HTML, documents etc.); \\
    9.22  
    9.23 -      @{executable "isabelle_process"} & run through @{tool_ref
    9.24 -      build}; \\
    9.25 +      @{tool_ref process} & run through @{tool_ref build}; \\
    9.26  
    9.27        @{tool_ref document} & run by the Isabelle process if document
    9.28        preparation is enabled; \\
    10.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 10 12:11:23 2016 +0100
    10.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 10 12:11:50 2016 +0100
    10.3 @@ -158,7 +158,7 @@
    10.4  if ($output_log) { print "Mirabelle: $thy_file\n"; }
    10.5  
    10.6  my $cmd =
    10.7 -  "\"$ENV{'ISABELLE_PROCESS'}\" " .
    10.8 +  "\"$ENV{'ISABELLE_TOOL'}\" process " .
    10.9    "-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
   10.10  my $result = system "bash", "-c", $cmd;
   10.11  
    11.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Mar 10 12:11:23 2016 +0100
    11.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Mar 10 12:11:50 2016 +0100
    11.3 @@ -133,7 +133,7 @@
    11.4  
    11.5  # execution
    11.6  
    11.7 -"$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
    11.8 +"$ISABELLE_TOOL" process -o auto_time_limit=10.0 \
    11.9    -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
   11.10  
   11.11  
    12.1 --- a/src/HOL/TPTP/CASC/ReadMe	Thu Mar 10 12:11:23 2016 +0100
    12.2 +++ b/src/HOL/TPTP/CASC/ReadMe	Thu Mar 10 12:11:50 2016 +0100
    12.3 @@ -180,7 +180,7 @@
    12.4  
    12.5    Then I ran
    12.6  
    12.7 -    ./bin/isabelle_process -e 'use_thy "/tmp/T";'  
    12.8 +    ./bin/isabelle process -e 'use_thy "/tmp/T";'  
    12.9  
   12.10    I also performed the aforementioned sanity tests.
   12.11  
    13.1 --- a/src/HOL/TPTP/lib/Tools/tptp_graph	Thu Mar 10 12:11:23 2016 +0100
    13.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Thu Mar 10 12:11:50 2016 +0100
    13.3 @@ -118,7 +118,7 @@
    13.4  begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
    13.5  ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
    13.6          > $WORKDIR/$LOADER.thy
    13.7 -  "$ISABELLE_PROCESS" -e "use_thy \"$WORKDIR/$LOADER\";" Pure
    13.8 +  "$ISABELLE_TOOL" process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
    13.9  }
   13.10  
   13.11  function cleanup_workdir()
    14.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Thu Mar 10 12:11:23 2016 +0100
    14.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Thu Mar 10 12:11:50 2016 +0100
    14.3 @@ -31,5 +31,5 @@
    14.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    14.5  ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    14.6      > /tmp/$SCRATCH.thy
    14.7 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    14.8 +  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    14.9  done
    15.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Thu Mar 10 12:11:23 2016 +0100
    15.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Thu Mar 10 12:11:50 2016 +0100
    15.3 @@ -31,5 +31,5 @@
    15.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    15.5  ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    15.6      > /tmp/$SCRATCH.thy
    15.7 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    15.8 +  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    15.9  done
    16.1 --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Thu Mar 10 12:11:23 2016 +0100
    16.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Thu Mar 10 12:11:50 2016 +0100
    16.3 @@ -31,5 +31,5 @@
    16.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    16.5  ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    16.6      > /tmp/$SCRATCH.thy
    16.7 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    16.8 +  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    16.9  done
    17.1 --- a/src/HOL/TPTP/lib/Tools/tptp_refute	Thu Mar 10 12:11:23 2016 +0100
    17.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Thu Mar 10 12:11:50 2016 +0100
    17.3 @@ -30,5 +30,5 @@
    17.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    17.5  ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    17.6      > /tmp/$SCRATCH.thy
    17.7 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    17.8 +  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    17.9  done
    18.1 --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Thu Mar 10 12:11:23 2016 +0100
    18.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Thu Mar 10 12:11:50 2016 +0100
    18.3 @@ -31,5 +31,5 @@
    18.4    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    18.5  ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
    18.6      > /tmp/$SCRATCH.thy
    18.7 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    18.8 +  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    18.9  done
    19.1 --- a/src/HOL/TPTP/lib/Tools/tptp_translate	Thu Mar 10 12:11:23 2016 +0100
    19.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Thu Mar 10 12:11:50 2016 +0100
    19.3 @@ -28,4 +28,4 @@
    19.4  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    19.5  ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
    19.6    > /tmp/$SCRATCH.thy
    19.7 -"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    19.8 +"$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
    20.1 --- a/src/Pure/Tools/ml_console.scala	Thu Mar 10 12:11:23 2016 +0100
    20.2 +++ b/src/Pure/Tools/ml_console.scala	Thu Mar 10 12:11:50 2016 +0100
    20.3 @@ -1,7 +1,7 @@
    20.4  /*  Title:      Pure/Tools/ml_console.scala
    20.5      Author:     Makarius
    20.6  
    20.7 -The raw ML process with interaction (line editor).
    20.8 +The raw ML process in interactive mode.
    20.9  */
   20.10  
   20.11  package isabelle
   20.12 @@ -33,11 +33,12 @@
   20.13      -m MODE      add print mode for output
   20.14      -n           no build of session image on startup
   20.15      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   20.16 -    -r           logic session is RAW_ML_SYSTEM
   20.17 +    -r           logic session is "RAW_ML_SYSTEM"
   20.18      -s           system build mode for session image
   20.19  
   20.20 -  Run Isabelle process with raw ML console and line editor
   20.21 -  (ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
   20.22 +  Build a logic session image and run the raw Isabelle ML process
   20.23 +  in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" +
   20.24 +  quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
   20.25  """,
   20.26          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   20.27          "l:" -> (arg => logic = arg),
    21.1 --- a/src/Pure/Tools/ml_process.scala	Thu Mar 10 12:11:23 2016 +0100
    21.2 +++ b/src/Pure/Tools/ml_process.scala	Thu Mar 10 12:11:50 2016 +0100
    21.3 @@ -36,7 +36,7 @@
    21.4          dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
    21.5            case Some(heap_path) => List(heap_path)
    21.6            case None =>
    21.7 -            error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
    21.8 +            error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
    21.9                cat_lines(dirs.map(dir => "  " + dir.implode)))
   21.10          }
   21.11        }
   21.12 @@ -124,7 +124,7 @@
   21.13        var options = Options.init()
   21.14  
   21.15        val getopts = Getopts("""
   21.16 -Usage: isabelle_process [OPTIONS] [HEAP]
   21.17 +Usage: isabelle process [OPTIONS] [HEAP]
   21.18  
   21.19    Options are:
   21.20      -e ML_EXPR   evaluate ML expression on startup
   21.21 @@ -132,15 +132,19 @@
   21.22      -m MODE      add print mode for output
   21.23      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   21.24  
   21.25 -  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
   21.26 -  $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
   21.27 -  if it is RAW_ML_SYSTEM, the initial ML heap is used.
   21.28 +  Run the raw Isabelle ML process in batch mode, using a given heap image.
   21.29 +
   21.30 +  If HEAP is a plain name (default ISABELLE_LOGIC=""" +
   21.31 +  quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in
   21.32 +  ISABELLE_PATH; if it contains a slash, it is taken as literal file;
   21.33 +  if it is "RAW_ML_SYSTEM", the initial ML heap is used.
   21.34  """,
   21.35          "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
   21.36          "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
   21.37          "m:" -> (arg => modes = arg :: modes),
   21.38          "o:" -> (arg => options = options + arg))
   21.39  
   21.40 +      if (args.isEmpty) getopts.usage()
   21.41        val heap =
   21.42          getopts(args) match {
   21.43            case Nil => ""
    22.1 --- a/src/Tools/Code/code_ml.ML	Thu Mar 10 12:11:23 2016 +0100
    22.2 +++ b/src/Tools/Code/code_ml.ML	Thu Mar 10 12:11:50 2016 +0100
    22.3 @@ -868,10 +868,10 @@
    22.4  val _ = Theory.setup
    22.5    (Code_Target.add_language
    22.6      (target_SML, { serializer = serializer_sml, literals = literals_sml,
    22.7 -      check = { env_var = "ISABELLE_PROCESS",
    22.8 +      check = { env_var = "ISABELLE_TOOL",
    22.9          make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
   22.10          make_command = fn _ =>
   22.11 -          "\"$ISABELLE_PROCESS\" -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
   22.12 +          "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
   22.13    #> Code_Target.add_language
   22.14      (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
   22.15        check = { env_var = "ISABELLE_OCAML",