src/Pure/ML/ml_process.scala
author wenzelm
Sun, 12 Nov 2017 12:41:05 +0100
changeset 67052 caf87d4b9b61
parent 67026 687c822ee5e3
child 67219 81e9804b2014
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65477
64e61b0f6972 clarified directories;
wenzelm
parents: 65471
diff changeset
     1
/*  Title:      Pure/ML/ml_process.scala
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     3
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
     4
The raw ML process.
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     5
*/
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     6
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     8
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     9
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    10
import java.io.{File => JFile}
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    11
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    12
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    13
object ML_Process
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    14
{
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    15
  def apply(options: Options,
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    16
    logic: String = "",
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    17
    args: List[String] = Nil,
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    18
    dirs: List[Path] = Nil,
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    19
    modes: List[String] = Nil,
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62639
diff changeset
    20
    raw_ml_system: Boolean = false,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    21
    cwd: JFile = null,
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62606
diff changeset
    22
    env: Map[String, String] = Isabelle_System.settings(),
62557
a4ea3a222e0e tuned signature;
wenzelm
parents: 62556
diff changeset
    23
    redirect: Boolean = false,
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
    24
    cleanup: () => Unit = () => (),
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62629
diff changeset
    25
    channel: Option[System_Channel] = None,
67052
caf87d4b9b61 tuned signature;
wenzelm
parents: 67026
diff changeset
    26
    sessions: Option[Sessions.Structure] = None,
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    27
    session_base: Option[Sessions.Base] = None,
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62629
diff changeset
    28
    store: Sessions.Store = Sessions.store()): Bash.Process =
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    29
  {
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    30
    val logic_name = Isabelle_System.default_logic(logic)
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    31
    val heaps: List[String] =
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62639
diff changeset
    32
      if (raw_ml_system) Nil
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    33
      else {
65419
457e4fbed731 explicit Sessions.Selection;
wenzelm
parents: 65415
diff changeset
    34
        val selection = Sessions.Selection(sessions = List(logic_name))
67025
961285f581e6 clarifified selection: always wrt. build_graph structure;
wenzelm
parents: 66961
diff changeset
    35
        val selected_sessions =
67026
687c822ee5e3 tuned signature;
wenzelm
parents: 67025
diff changeset
    36
          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
66848
982baed14542 clarified signature;
wenzelm
parents: 66782
diff changeset
    37
        selected_sessions.build_requirements(List(logic_name)).
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    38
          map(a => File.platform_path(store.heap(a)))
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    39
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    40
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    41
    val eval_init =
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    42
      if (heaps.isEmpty) {
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    43
        List(
62912
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    44
          """
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    45
          fun chapter (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    46
          fun section (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    47
          fun subsection (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    48
          fun subsubsection (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    49
          fun paragraph (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    50
          fun subparagraph (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    51
          val ML_file = PolyML.use;
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    52
          """,
64557
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    53
          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    54
            """
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    55
              structure FixedInt = IntInf;
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    56
              structure RunCall =
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    57
              struct
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    58
                open RunCall
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    59
                val loadWord: word * word -> word =
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    60
                  run_call2 RuntimeCalls.POLY_SYS_load_word;
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    61
                val storeWord: word * word * word -> unit =
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    62
                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    63
              end;
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 64304
diff changeset
    64
            """
62855
82859dac5f59 clarified bootstrap -- avoid conditional compilation in ROOT.ML;
wenzelm
parents: 62835
diff changeset
    65
          else "",
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    66
          if (Platform.is_windows)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    67
            "fun exit 0 = OS.Process.exit OS.Process.success" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    68
            " | exit 1 = OS.Process.exit OS.Process.failure" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    69
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    70
          else
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    71
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
62629
1815513a57f1 clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents: 62614
diff changeset
    72
          "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
1815513a57f1 clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents: 62614
diff changeset
    73
          "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    74
      }
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    75
      else
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    76
        List(
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    77
          "(PolyML.SaveState.loadHierarchy " +
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
    78
            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    79
          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
    80
          ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    81
          "); OS.Process.exit OS.Process.failure)")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    82
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    83
    val eval_modes =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    84
      if (modes.isEmpty) Nil
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
    85
      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    86
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    87
    // options
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    88
    val isabelle_process_options = Isabelle_System.tmp_file("options")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    89
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    90
    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    91
    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    92
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    93
    // session base
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    94
    val eval_session_base =
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    95
      session_base match {
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    96
        case None => Nil
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    97
        case Some(base) =>
65441
9425e4d8bdb6 more session_base information in ML;
wenzelm
parents: 65432
diff changeset
    98
          def print_table(table: List[(String, String)]): String =
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    99
            ML_Syntax.print_list(
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   100
              ML_Syntax.print_pair(
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
   101
                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
66712
4c98c929a12a session-qualified theory names are mandatory;
wenzelm
parents: 65532
diff changeset
   102
          def print_list(list: List[String]): String =
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
   103
            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
65532
febfd9f78bd4 eliminated default_qualifier: just a constant;
wenzelm
parents: 65478
diff changeset
   104
          List("Resources.init_session_base" +
febfd9f78bd4 eliminated default_qualifier: just a constant;
wenzelm
parents: 65478
diff changeset
   105
            " {global_theories = " + print_table(base.global_theories.toList) +
66717
67dbf5cdc056 more informative loaded_theories: dependencies and syntax;
wenzelm
parents: 66712
diff changeset
   106
            ", loaded_theories = " + print_list(base.loaded_theories.keys) +
65441
9425e4d8bdb6 more session_base information in ML;
wenzelm
parents: 65432
diff changeset
   107
            ", known_theories = " + print_table(base.dest_known_theories) + "}")
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   108
      }
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   109
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   110
    // process
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   111
    val eval_process =
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   112
      if (heaps.isEmpty)
62712
22a17cec2efe clarified use of options;
wenzelm
parents: 62711
diff changeset
   113
        List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
   114
      else
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
   115
        channel match {
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
   116
          case None =>
62712
22a17cec2efe clarified use of options;
wenzelm
parents: 62711
diff changeset
   117
            List("Isabelle_Process.init_options ()")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
   118
          case Some(ch) =>
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
   119
            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_bytes(ch.server_name))
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
   120
        }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   121
62601
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   122
    // ISABELLE_TMP
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   123
    val isabelle_tmp = Isabelle_System.tmp_dir("process")
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   124
    val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   125
64274
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   126
    val ml_runtime_options =
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   127
    {
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   128
      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   129
      if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   130
      else ml_options ::: List("--gcthreads", options.int("threads").toString)
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   131
    }
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   132
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
   133
    // bash
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
   134
    val bash_args =
64274
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   135
      ml_runtime_options :::
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   136
      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
   137
        map(eval => List("--eval", eval)).flatten ::: args
62546
wenzelm
parents: 62545
diff changeset
   138
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62912
diff changeset
   139
    Bash.process(
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62912
diff changeset
   140
      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64274
diff changeset
   141
        Bash.strings(bash_args),
62614
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   142
      cwd = cwd,
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   143
      env =
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   144
        Isabelle_System.library_path(env ++ env_options ++ env_tmp,
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   145
          Isabelle_System.getenv_strict("ML_HOME")),
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   146
      redirect = redirect,
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   147
      cleanup = () =>
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   148
        {
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   149
          isabelle_process_options.delete
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   150
          Isabelle_System.rm_tree(isabelle_tmp)
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
   151
          cleanup()
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   152
        })
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   153
  }
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   154
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   155
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   156
  /* Isabelle tool wrapper */
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   157
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   158
  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   159
  {
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   160
    var dirs: List[Path] = Nil
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   161
    var eval_args: List[String] = Nil
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   162
    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   163
    var modes: List[String] = Nil
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   164
    var options = Options.init()
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   165
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   166
    val getopts = Getopts("""
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   167
Usage: isabelle process [OPTIONS]
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   168
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   169
  Options are:
62677
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62672
diff changeset
   170
    -T THEORY    load theory
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62638
diff changeset
   171
    -d DIR       include session directory
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   172
    -e ML_EXPR   evaluate ML expression on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   173
    -f ML_FILE   evaluate ML file on startup
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   174
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   175
    -m MODE      add print mode for output
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   176
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   177
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   178
  Run the raw Isabelle ML process in batch mode.
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   179
""",
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   180
      "T:" -> (arg =>
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
   181
        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   182
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   183
      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   184
      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   185
      "l:" -> (arg => logic = arg),
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   186
      "m:" -> (arg => modes = arg :: modes),
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   187
      "o:" -> (arg => options = options + arg))
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   188
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   189
    val more_args = getopts(args)
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   190
    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   191
62888
64f44d7279e5 proper return code;
wenzelm
parents: 62855
diff changeset
   192
    val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   193
      result().print_stdout.rc
62888
64f44d7279e5 proper return code;
wenzelm
parents: 62855
diff changeset
   194
    sys.exit(rc)
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   195
  })
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   196
}