1/*  Title:      Pure/ML/ml_process.scala
2    Author:     Makarius
3
4The raw ML process.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object ML_Process
14{
15  def apply(options: Options,
16    logic: String = "",
17    args: List[String] = Nil,
18    dirs: List[Path] = Nil,
19    modes: List[String] = Nil,
20    raw_ml_system: Boolean = false,
21    cwd: JFile = null,
22    env: Map[String, String] = Isabelle_System.settings(),
23    redirect: Boolean = false,
24    cleanup: () => Unit = () => (),
25    sessions_structure: Option[Sessions.Structure] = None,
26    session_base: Option[Sessions.Base] = None,
27    store: Option[Sessions.Store] = None): Bash.Process =
28  {
29    val logic_name = Isabelle_System.default_logic(logic)
30    val _store = store.getOrElse(Sessions.store(options))
31
32    val sessions_structure1 =
33      sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
34
35    val heaps: List[String] =
36      if (raw_ml_system) Nil
37      else {
38        sessions_structure1.selection(Sessions.Selection.session(logic_name)).
39          build_requirements(List(logic_name)).
40          map(a => File.platform_path(_store.the_heap(a)))
41      }
42
43    val eval_init =
44      if (heaps.isEmpty) {
45        List(
46          """
47          fun chapter (_: string) = ();
48          fun section (_: string) = ();
49          fun subsection (_: string) = ();
50          fun subsubsection (_: string) = ();
51          fun paragraph (_: string) = ();
52          fun subparagraph (_: string) = ();
53          val ML_file = PolyML.use;
54          """,
55          if (Platform.is_windows)
56            "fun exit 0 = OS.Process.exit OS.Process.success" +
57            " | exit 1 = OS.Process.exit OS.Process.failure" +
58            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
59          else
60            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
61          "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
62          "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
63      }
64      else
65        List(
66          "(PolyML.SaveState.loadHierarchy " +
67            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
68          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
69          ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
70          "); OS.Process.exit OS.Process.failure)")
71
72    val eval_modes =
73      if (modes.isEmpty) Nil
74      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
75
76    // options
77    val isabelle_process_options = Isabelle_System.tmp_file("options")
78    Isabelle_System.chmod("600", File.path(isabelle_process_options))
79    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
80    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
81    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
82
83    // session base
84    val eval_session_base =
85      session_base match {
86        case None => Nil
87        case Some(base) =>
88          def print_table(table: List[(String, String)]): String =
89            ML_Syntax.print_list(
90              ML_Syntax.print_pair(
91                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
92          def print_list(list: List[String]): String =
93            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
94          def print_sessions(list: List[(String, Position.T)]): String =
95            ML_Syntax.print_list(
96              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
97
98          List("Resources.init_session_base" +
99            " {session_positions = " + print_sessions(sessions_structure1.session_positions) +
100            ", session_directories = " + print_table(sessions_structure1.dest_session_directories) +
101            ", docs = " + print_list(base.doc_names) +
102            ", global_theories = " + print_table(base.global_theories.toList) +
103            ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
104      }
105
106    // process
107    val eval_process =
108      if (heaps.isEmpty)
109        List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
110      else List("Isabelle_Process.init ()")
111
112    // ISABELLE_TMP
113    val isabelle_tmp = Isabelle_System.tmp_dir("process")
114    val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
115
116    val ml_runtime_options =
117    {
118      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
119      val ml_options1 =
120        if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
121        else ml_options ::: List("--gcthreads", options.int("threads").toString)
122      val ml_options2 =
123        if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
124        else ml_options1 ::: List("--codepage", "utf8")
125      ml_options2
126    }
127
128    // bash
129    val bash_args =
130      ml_runtime_options :::
131      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
132        .flatMap(eval => List("--eval", eval)) ::: args
133
134    Bash.process(
135      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
136        Bash.strings(bash_args),
137      cwd = cwd,
138      env = env ++ env_options ++ env_tmp,
139      redirect = redirect,
140      cleanup = () =>
141        {
142          isabelle_process_options.delete
143          Isabelle_System.rm_tree(isabelle_tmp)
144          cleanup()
145        })
146  }
147
148
149  /* Isabelle tool wrapper */
150
151  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
152  {
153    var dirs: List[Path] = Nil
154    var eval_args: List[String] = Nil
155    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
156    var modes: List[String] = Nil
157    var options = Options.init()
158
159    val getopts = Getopts("""
160Usage: isabelle process [OPTIONS]
161
162  Options are:
163    -T THEORY    load theory
164    -d DIR       include session directory
165    -e ML_EXPR   evaluate ML expression on startup
166    -f ML_FILE   evaluate ML file on startup
167    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
168    -m MODE      add print mode for output
169    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
170
171  Run the raw Isabelle ML process in batch mode.
172""",
173      "T:" -> (arg =>
174        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
175      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
176      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
177      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
178      "l:" -> (arg => logic = arg),
179      "m:" -> (arg => modes = arg :: modes),
180      "o:" -> (arg => options = options + arg))
181
182    val more_args = getopts(args)
183    if (args.isEmpty || more_args.nonEmpty) getopts.usage()
184
185    val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
186      result().print_stdout.rc
187    sys.exit(rc)
188  })
189}
190