# HG changeset patch
# User wenzelm
# Date 1458125125 -3600
# Node ID aa3b47b321004cb0e1fa6c53cc6bb062424ecf48
# Parent  e57416b649d5f0612a013bb976608184ec1650e1
less physical "logic" argument, with option -l like "isabelle console" etc.;

diff -r e57416b649d5 -r aa3b47b32100 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Doc/System/Basics.thy	Wed Mar 16 11:45:25 2016 +0100
@@ -302,24 +302,16 @@
 text \<open>
   The @{tool_def process} tool runs the raw ML process in batch mode:
   @{verbatim [display]
-\<open>Usage: isabelle process [OPTIONS] [HEAP]
+\<open>Usage: isabelle process [OPTIONS]
 
   Options are:
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
+    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
 
-  Run the raw Isabelle ML process in batch mode, using a given heap image.
-
-  If HEAP is a plain name (default ISABELLE_LOGIC), it is searched in
-  ISABELLE_PATH; if it contains a slash, it is taken as literal file;
-  if it is RAW_ML_SYSTEM, the initial ML heap is used.\<close>}
-
-  Heap files without explicit directory specifications are looked up in the
-  @{setting ISABELLE_PATH} setting, which may consist of multiple components
-  separated by colons --- these are tried in the given order with the value of
-  @{setting ML_IDENTIFIER} appended internally.
+  Run the raw Isabelle ML process in batch mode.\<close>}
 \<close>
 
 
@@ -332,6 +324,9 @@
   premature exit of the ML process with return code 1.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-l\<close> specifies the logic session name.
+
+  \<^medskip>
   The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
   session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
   mathematical Isabelle symbols.
@@ -347,7 +342,7 @@
 text \<open>
   The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
   loader within ML:
-  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"' HOL\<close>}
+  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
 
   Observe the delicate quoting rules for the Bash shell vs.\ ML. The
   Isabelle/ML and Scala libraries provide functions for that, but here we need
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Mar 16 11:45:25 2016 +0100
@@ -159,7 +159,7 @@
 
 my $cmd =
   "isabelle process -o quick_and_dirty -o threads=1" .
-  " -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
+  " -e 'use_thy \"$path/$new_thy_name\"' -l $mirabelle_logic" . $quiet;
 my $result = system "bash", "-c", $cmd;
 
 if ($output_log) {
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_graph
--- a/src/HOL/TPTP/lib/Tools/tptp_graph	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Wed Mar 16 11:45:25 2016 +0100
@@ -118,7 +118,7 @@
 begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
 ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
         > $WORKDIR/$LOADER.thy
-  isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
+  isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" -l Pure
 }
 
 function cleanup_workdir()
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_isabelle
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Wed Mar 16 11:45:25 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  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.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l 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.$"
 done
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Wed Mar 16 11:45:25 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  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.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l 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.$"
 done
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_nitpick
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Wed Mar 16 11:45:25 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  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.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l 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.$"
 done
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_refute
--- a/src/HOL/TPTP/lib/Tools/tptp_refute	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Wed Mar 16 11:45:25 2016 +0100
@@ -30,5 +30,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  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.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l 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.$"
 done
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_sledgehammer
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Wed Mar 16 11:45:25 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  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.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l 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.$"
 done
diff -r e57416b649d5 -r aa3b47b32100 src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Wed Mar 16 11:45:25 2016 +0100
@@ -28,4 +28,4 @@
 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
   > /tmp/$SCRATCH.thy
-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.$"
+isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l 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.$"
diff -r e57416b649d5 -r aa3b47b32100 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Wed Mar 16 11:45:25 2016 +0100
@@ -58,7 +58,7 @@
       }
 
     prover_session.start(receiver =>
-      Isabelle_Process(options, heap = parent_session, receiver = receiver))
+      Isabelle_Process(options, logic = parent_session, receiver = receiver))
 
     batch_session
   }
diff -r e57416b649d5 -r aa3b47b32100 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Wed Mar 16 11:45:25 2016 +0100
@@ -11,7 +11,7 @@
 {
   def apply(
     options: Options,
-    heap: String = "",
+    logic: String = "",
     args: List[String] = Nil,
     modes: List[String] = Nil,
     secure: Boolean = false,
@@ -21,7 +21,7 @@
     val channel = System_Channel()
     val process =
       try {
-        ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
+        ML_Process(options, logic = logic, args = args, modes = modes, secure = secure,
           channel = Some(channel), store = store)
       }
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
diff -r e57416b649d5 -r aa3b47b32100 src/Pure/Tools/ml_console.scala
--- a/src/Pure/Tools/ml_console.scala	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala	Wed Mar 16 11:45:25 2016 +0100
@@ -69,7 +69,7 @@
 
       // process loop
       val process =
-        ML_Process(options, heap = logic, args = List("-i"),
+        ML_Process(options, logic = logic, args = List("-i"),
           modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"),
           store = Sessions.store(system_mode))
       val process_output = Future.thread[Unit]("process_output") {
diff -r e57416b649d5 -r aa3b47b32100 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 11:45:25 2016 +0100
@@ -13,7 +13,7 @@
 object ML_Process
 {
   def apply(options: Options,
-    heap: String = "",
+    logic: String = "",
     args: List[String] = Nil,
     modes: List[String] = Nil,
     secure: Boolean = false,
@@ -24,34 +24,27 @@
     channel: Option[System_Channel] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
-    val load_heaps =
-    {
-      if (heap == "RAW_ML_SYSTEM") Nil
-      else if (heap.iterator.contains('/')) {
-        val heap_path = Path.explode(heap)
-        if (!heap_path.is_file) error("Bad heap file: " + heap_path)
-        List(heap_path)
+    val heaps =
+      Isabelle_System.default_logic(logic) match {
+        case "RAW_ML_SYSTEM" => Nil
+        case name =>
+          store.find_heap(name) match {
+            case Some(path) => List(path)
+            case None =>
+              error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
+                cat_lines(store.input_dirs.map(dir => "  " + dir.implode)))
+          }
       }
-      else {
-        val heap_name = Isabelle_System.default_logic(heap)
-        store.find_heap(heap_name) match {
-          case Some(heap_path) => List(heap_path)
-          case None =>
-            error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
-              cat_lines(store.input_dirs.map(dir => "  " + dir.implode)))
-        }
-      }
-    }
 
     val eval_heaps =
-      load_heaps.map(load_heap =>
-        "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
+      heaps.map(heap =>
+        "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(heap)) +
         "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
-        ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
+        ML_Syntax.print_string_raw(": " + heap.toString + "\n") +
         "); OS.Process.exit OS.Process.failure)")
 
     val eval_initial =
-      if (load_heaps.isEmpty) {
+      if (heaps.isEmpty) {
         List(
           if (Platform.is_windows)
             "fun exit 0 = OS.Process.exit OS.Process.success" +
@@ -72,12 +65,12 @@
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
-    val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
+    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
     val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
 
     val eval_process =
-      if (load_heaps.isEmpty)
+      if (heaps.isEmpty)
         List("PolyML.print_depth 10")
       else
         channel match {
@@ -119,39 +112,32 @@
   {
     Command_Line.tool {
       var eval_args: List[String] = Nil
+      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
       var modes: List[String] = Nil
       var options = Options.init()
 
       val getopts = Getopts("""
-Usage: isabelle process [OPTIONS] [HEAP]
+Usage: isabelle process [OPTIONS]
 
   Options are:
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
+    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
 
-  Run the raw Isabelle ML process in batch mode, using a given heap image.
-
-  If HEAP is a plain name (default ISABELLE_LOGIC=""" +
-  quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in
-  ISABELLE_PATH; if it contains a slash, it is taken as literal file;
-  if it is "RAW_ML_SYSTEM", the initial ML heap is used.
+  Run the raw Isabelle ML process in batch mode.
 """,
         "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
         "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+        "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
         "o:" -> (arg => options = options + arg))
 
-      if (args.isEmpty) getopts.usage()
-      val heap =
-        getopts(args) match {
-          case Nil => ""
-          case List(heap) => heap
-          case _ => getopts.usage()
-        }
+      val more_args = getopts(args)
+      if (args.isEmpty || !more_args.isEmpty) getopts.usage()
 
-      ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
+      ML_Process(options, logic = logic, args = eval_args ::: args.toList, modes = modes).
         result().print_stdout.rc
     }
   }
diff -r e57416b649d5 -r aa3b47b32100 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Tools/Code/code_ml.ML	Wed Mar 16 11:45:25 2016 +0100
@@ -871,7 +871,7 @@
       check = { env_var = "ISABELLE_TOOL",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn _ =>
-          "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' Pure" } })
+          "\"$ISABELLE_TOOL\" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure" } })
   #> Code_Target.add_language
     (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "ISABELLE_OCAML",
diff -r e57416b649d5 -r aa3b47b32100 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 15 23:59:39 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Mar 16 11:45:25 2016 +0100
@@ -76,7 +76,7 @@
        space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
     PIDE.session.start(receiver =>
       Isabelle_Process(
-        PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver,
+        PIDE.options.value, logic = session_name(), modes = modes, receiver = receiver,
         store = Sessions.store(session_build_mode() == "system")))
   }