src/Pure/ML/ml_process.scala
author wenzelm
Sun, 15 Nov 2020 22:04:16 +0100
changeset 72854 5fc193537b7c
parent 72853 217e6cf61453
child 72859 429afd0d1a79
permissions -rw-r--r--
tuned;
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,
71809
8a298184f3f9 clarified signature;
wenzelm
parents: 71592
diff changeset
    16
    sessions_structure: Sessions.Structure,
71813
269dc4bf1f40 clarified signature;
wenzelm
parents: 71809
diff changeset
    17
    store: Sessions.Store,
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    18
    logic: String = "",
71854
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
    19
    raw_ml_system: Boolean = false,
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
    20
    use_prelude: List[String] = Nil,
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
    21
    eval_main: String = "",
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    22
    args: List[String] = Nil,
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    23
    modes: List[String] = Nil,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    24
    cwd: JFile = null,
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62606
diff changeset
    25
    env: Map[String, String] = Isabelle_System.settings(),
62557
a4ea3a222e0e tuned signature;
wenzelm
parents: 62556
diff changeset
    26
    redirect: Boolean = false,
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
    27
    cleanup: () => Unit = () => (),
71813
269dc4bf1f40 clarified signature;
wenzelm
parents: 71809
diff changeset
    28
    session_base: Option[Sessions.Base] = None): 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)
68209
aeffd8f1f079 support Store with options;
wenzelm
parents: 68204
diff changeset
    31
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    32
    val heaps: List[String] =
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62639
diff changeset
    33
      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
    34
      else {
72806
ab4a0b19648a tuned signature;
wenzelm
parents: 72793
diff changeset
    35
        sessions_structure.selection(logic_name).
70873
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70012
diff changeset
    36
          build_requirements(List(logic_name)).
71813
269dc4bf1f40 clarified signature;
wenzelm
parents: 71809
diff changeset
    37
          map(a => File.platform_path(store.the_heap(a)))
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    38
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    39
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    40
    val eval_init =
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    41
      if (heaps.isEmpty) {
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    42
        List(
62912
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    43
          """
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    44
          fun chapter (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    45
          fun section (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    46
          fun subsection (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    47
          fun subsubsection (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    48
          fun paragraph (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    49
          fun subparagraph (_: string) = ();
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    50
          val ML_file = PolyML.use;
745d31e63c21 section headings for ROOT.ML;
wenzelm
parents: 62902
diff changeset
    51
          """,
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    52
          if (Platform.is_windows)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    53
            "fun exit 0 = OS.Process.exit OS.Process.success" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    54
            " | exit 1 = OS.Process.exit OS.Process.failure" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    55
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    56
          else
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    57
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
62629
1815513a57f1 clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents: 62614
diff changeset
    58
          "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
1815513a57f1 clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents: 62614
diff changeset
    59
          "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    60
      }
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    61
      else
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    62
        List(
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    63
          "(PolyML.SaveState.loadHierarchy " +
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
    64
            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
    65
          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
    66
          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
    67
          "); OS.Process.exit OS.Process.failure)")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    68
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    69
    val eval_modes =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    70
      if (modes.isEmpty) Nil
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
    71
      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
    72
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    73
    // options
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    74
    val isabelle_process_options = Isabelle_System.tmp_file("options")
71313
6cfec8029831 clarified signature;
wenzelm
parents: 70978
diff changeset
    75
    Isabelle_System.chmod("600", File.path(isabelle_process_options))
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    76
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    77
    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
    78
    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
    79
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    80
    // session base
72852
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
    81
    val init_session = Isabelle_System.tmp_file("init_session", ext = "ML")
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
    82
    val init_session_name = init_session.getAbsolutePath
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
    83
    Isabelle_System.chmod("600", File.path(init_session))
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
    84
    File.write(init_session,
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    85
      session_base match {
72852
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
    86
        case None => ""
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    87
        case Some(base) =>
72854
wenzelm
parents: 72853
diff changeset
    88
          def print_table: List[(String, String)] => String =
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    89
            ML_Syntax.print_list(
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
    90
              ML_Syntax.print_pair(
72854
wenzelm
parents: 72853
diff changeset
    91
                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))
72851
wenzelm
parents: 72850
diff changeset
    92
          def print_list: List[String] => String =
wenzelm
parents: 72850
diff changeset
    93
            ML_Syntax.print_list(ML_Syntax.print_string_bytes)
wenzelm
parents: 72850
diff changeset
    94
          def print_sessions: List[(String, Position.T)] => String =
67493
c4e9e0c50487 treat sessions as entities with defining position;
wenzelm
parents: 67472
diff changeset
    95
            ML_Syntax.print_list(
72851
wenzelm
parents: 72850
diff changeset
    96
              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))
wenzelm
parents: 72850
diff changeset
    97
          def print_bibtex_entries: List[(String, List[String])] => String =
72850
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72806
diff changeset
    98
            ML_Syntax.print_list(
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72806
diff changeset
    99
              ML_Syntax.print_pair(ML_Syntax.print_string_bytes,
72851
wenzelm
parents: 72850
diff changeset
   100
                ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
67493
c4e9e0c50487 treat sessions as entities with defining position;
wenzelm
parents: 67472
diff changeset
   101
72852
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   102
          "Resources.init_session" +
72348
84f716e72fa3 adapted to 7b318273a4aa;
wenzelm
parents: 72342
diff changeset
   103
            "{session_positions = " + print_sessions(sessions_structure.session_positions) +
71809
8a298184f3f9 clarified signature;
wenzelm
parents: 71592
diff changeset
   104
            ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
72853
217e6cf61453 refer to session structure from resources;
wenzelm
parents: 72852
diff changeset
   105
            ", session_chapters = " + print_table(sessions_structure.session_chapters) +
72850
d01ea9e3bd2d clarified bibtex_entries: refer to overall session structure;
wenzelm
parents: 72806
diff changeset
   106
            ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
67520
6ff47e27c32d proper signature (amending c4e9e0c50487);
wenzelm
parents: 67493
diff changeset
   107
            ", docs = " + print_list(base.doc_names) +
67219
81e9804b2014 added document antiquotation @{session name};
wenzelm
parents: 67052
diff changeset
   108
            ", global_theories = " + print_table(base.global_theories.toList) +
72852
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   109
            ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}"
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   110
      })
65431
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   111
4a3e6cda3b94 provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents: 65420
diff changeset
   112
    // process
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   113
    val eval_process =
71854
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
   114
      proper_string(eval_main).getOrElse(
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
   115
        if (heaps.isEmpty) {
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
   116
          "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
   117
        }
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
   118
        else "Isabelle_Process.init ()")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   119
62601
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   120
    // ISABELLE_TMP
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   121
    val isabelle_tmp = Isabelle_System.tmp_dir("process")
72349
d115d50a19c0 provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents: 72348
diff changeset
   122
    val env_tmp =
d115d50a19c0 provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents: 72348
diff changeset
   123
      Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp),
d115d50a19c0 provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents: 72348
diff changeset
   124
        "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath)
62601
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
   125
72107
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 72102
diff changeset
   126
    val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 72102
diff changeset
   127
64274
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   128
    val ml_runtime_options =
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   129
    {
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   130
      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
69718
1adc89c4a795 clarified ML_OPTIONS on Windows;
wenzelm
parents: 69585
diff changeset
   131
      val ml_options1 =
1adc89c4a795 clarified ML_OPTIONS on Windows;
wenzelm
parents: 69585
diff changeset
   132
        if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
1adc89c4a795 clarified ML_OPTIONS on Windows;
wenzelm
parents: 69585
diff changeset
   133
        else ml_options ::: List("--gcthreads", options.int("threads").toString)
1adc89c4a795 clarified ML_OPTIONS on Windows;
wenzelm
parents: 69585
diff changeset
   134
      val ml_options2 =
1adc89c4a795 clarified ML_OPTIONS on Windows;
wenzelm
parents: 69585
diff changeset
   135
        if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
1adc89c4a795 clarified ML_OPTIONS on Windows;
wenzelm
parents: 69585
diff changeset
   136
        else ml_options1 ::: List("--codepage", "utf8")
72342
3546dd4ade74 ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents: 72107
diff changeset
   137
      ml_options2 ::: List("--exportstats")
64274
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   138
    }
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   139
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
   140
    // 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
   141
    val bash_args =
64274
c8990e5feac9 re-use "threads" for --gcthreads;
wenzelm
parents: 63986
diff changeset
   142
      ml_runtime_options :::
72852
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   143
      (eval_init ::: eval_modes ::: eval_options).flatMap(List("--eval", _)) :::
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   144
      List("--use", init_session_name,
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   145
        "--eval", "OS.FileSys.remove " + ML_Syntax.print_string_bytes(init_session_name)) :::
71854
ec84f542e411 clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents: 71813
diff changeset
   146
      use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
62546
wenzelm
parents: 62545
diff changeset
   147
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62912
diff changeset
   148
    Bash.process(
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62912
diff changeset
   149
      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64274
diff changeset
   150
        Bash.strings(bash_args),
62614
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   151
      cwd = cwd,
72107
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 72102
diff changeset
   152
      env = env ++ env_options ++ env_tmp ++ env_functions,
62614
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   153
      redirect = redirect,
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   154
      cleanup = () =>
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   155
        {
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   156
          isabelle_process_options.delete
72852
f827c3bb6b7f more scalable: avoid large strings on command-line;
wenzelm
parents: 72851
diff changeset
   157
          init_session.delete
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   158
          Isabelle_System.rm_tree(isabelle_tmp)
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
   159
          cleanup()
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   160
        })
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   161
  }
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   162
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   163
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   164
  /* Isabelle tool wrapper */
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 isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   167
  {
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   168
    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
   169
    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
   170
    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
   171
    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
   172
    var options = Options.init()
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   173
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   174
    val getopts = Getopts("""
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   175
Usage: isabelle process [OPTIONS]
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   176
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   177
  Options are:
62677
0df43889f496 isabelle process -T THEORY;
wenzelm
parents: 62672
diff changeset
   178
    -T THEORY    load theory
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62638
diff changeset
   179
    -d DIR       include session directory
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   180
    -e ML_EXPR   evaluate ML expression on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   181
    -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
   182
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   183
    -m MODE      add print mode for output
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   184
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   185
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   186
  Run the raw Isabelle ML process in batch mode.
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   187
""",
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   188
      "T:" -> (arg =>
66782
193c31b79a33 clarified signature;
wenzelm
parents: 66781
diff changeset
   189
        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
   190
      "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
   191
      "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
   192
      "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
   193
      "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
   194
      "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
   195
      "o:" -> (arg => options = options + arg))
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   196
62835
1a9ce1b13b20 prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents: 62712
diff changeset
   197
    val more_args = getopts(args)
71592
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 71313
diff changeset
   198
    if (args.isEmpty || more_args.nonEmpty) getopts.usage()
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   199
71809
8a298184f3f9 clarified signature;
wenzelm
parents: 71592
diff changeset
   200
    val sessions_structure = Sessions.load_structure(options, dirs = dirs)
71813
269dc4bf1f40 clarified signature;
wenzelm
parents: 71809
diff changeset
   201
    val store = Sessions.store(options)
71809
8a298184f3f9 clarified signature;
wenzelm
parents: 71592
diff changeset
   202
72793
6345cce0e576 clarified output of "isabelle process";
wenzelm
parents: 72349
diff changeset
   203
    val result =
71813
269dc4bf1f40 clarified signature;
wenzelm
parents: 71809
diff changeset
   204
      ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
72793
6345cce0e576 clarified output of "isabelle process";
wenzelm
parents: 72349
diff changeset
   205
        .result(
6345cce0e576 clarified output of "isabelle process";
wenzelm
parents: 72349
diff changeset
   206
          progress_stdout = Output.writeln(_, stdout = true),
6345cce0e576 clarified output of "isabelle process";
wenzelm
parents: 72349
diff changeset
   207
          progress_stderr = Output.writeln(_))
6345cce0e576 clarified output of "isabelle process";
wenzelm
parents: 72349
diff changeset
   208
6345cce0e576 clarified output of "isabelle process";
wenzelm
parents: 72349
diff changeset
   209
    sys.exit(result.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
   210
  })
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   211
}