diff -r a72ae9eb4462 -r 64e61b0f6972 src/Pure/Tools/ml_process.scala --- a/src/Pure/Tools/ml_process.scala Thu Apr 13 12:19:28 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,194 +0,0 @@ -/* Title: Pure/Tools/ml_process.scala - Author: Makarius - -The raw ML process. -*/ - -package isabelle - - -import java.io.{File => JFile} - - -object ML_Process -{ - def apply(options: Options, - logic: String = "", - args: List[String] = Nil, - dirs: List[Path] = Nil, - modes: List[String] = Nil, - raw_ml_system: Boolean = false, - cwd: JFile = null, - env: Map[String, String] = Isabelle_System.settings(), - redirect: Boolean = false, - cleanup: () => Unit = () => (), - channel: Option[System_Channel] = None, - sessions: Option[Sessions.T] = None, - session_base: Option[Sessions.Base] = None, - store: Sessions.Store = Sessions.store()): Bash.Process = - { - val logic_name = Isabelle_System.default_logic(logic) - val heaps: List[String] = - if (raw_ml_system) Nil - else { - val selection = Sessions.Selection(sessions = List(logic_name)) - val (_, selected_sessions) = - sessions.getOrElse(Sessions.load(options, dirs)).selection(selection) - (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)). - map(a => File.platform_path(store.heap(a))) - } - - val eval_init = - if (heaps.isEmpty) { - List( - """ - fun chapter (_: string) = (); - fun section (_: string) = (); - fun subsection (_: string) = (); - fun subsubsection (_: string) = (); - fun paragraph (_: string) = (); - fun subparagraph (_: string) = (); - val ML_file = PolyML.use; - """, - if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") - """ - structure FixedInt = IntInf; - structure RunCall = - struct - open RunCall - val loadWord: word * word -> word = - run_call2 RuntimeCalls.POLY_SYS_load_word; - val storeWord: word * word * word -> unit = - run_call3 RuntimeCalls.POLY_SYS_assign_word; - end; - """ - else "", - if (Platform.is_windows) - "fun exit 0 = OS.Process.exit OS.Process.success" + - " | exit 1 = OS.Process.exit OS.Process.failure" + - " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" - else - "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", - "PolyML.Compiler.prompt1 := \"Poly/ML> \"", - "PolyML.Compiler.prompt2 := \"Poly/ML# \"") - } - else - List( - "(PolyML.SaveState.loadHierarchy " + - ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) + - "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + - ML_Syntax.print_string0(": " + logic_name + "\n") + - "); OS.Process.exit OS.Process.failure)") - - val eval_modes = - if (modes.isEmpty) Nil - else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes)) - - // options - 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 (heaps.isEmpty) Nil else List("Options.load_default ()") - - // session base - val eval_session_base = - session_base match { - case None => Nil - case Some(base) => - def print_table(table: List[(String, String)]): String = - ML_Syntax.print_list( - ML_Syntax.print_pair( - ML_Syntax.print_string, ML_Syntax.print_string))(table) - List("Resources.set_session_base {default_qualifier = \"\"" + - ", global_theories = " + print_table(base.global_theories.toList) + - ", loaded_theories = " + print_table(base.loaded_theories.toList) + - ", known_theories = " + print_table(base.dest_known_theories) + "}") - } - - // process - val eval_process = - if (heaps.isEmpty) - List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))) - else - channel match { - case None => - List("Isabelle_Process.init_options ()") - case Some(ch) => - List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name)) - } - - // ISABELLE_TMP - val isabelle_tmp = Isabelle_System.tmp_dir("process") - val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) - - val ml_runtime_options = - { - val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) - if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options - else ml_options ::: List("--gcthreads", options.int("threads").toString) - } - - // bash - val bash_args = - ml_runtime_options ::: - (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process). - map(eval => List("--eval", eval)).flatten ::: args - - Bash.process( - "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + - Bash.strings(bash_args), - cwd = cwd, - env = - Isabelle_System.library_path(env ++ env_options ++ env_tmp, - Isabelle_System.getenv_strict("ML_HOME")), - redirect = redirect, - cleanup = () => - { - isabelle_process_options.delete - Isabelle_System.rm_tree(isabelle_tmp) - cleanup() - }) - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => - { - var dirs: List[Path] = Nil - 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] - - Options are: - -T THEORY load theory - -d DIR include session directory - -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. -""", - "T:" -> (arg => - eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "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)) - - val more_args = getopts(args) - if (args.isEmpty || !more_args.isEmpty) getopts.usage() - - val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). - result().print_stdout.rc - sys.exit(rc) - }) -}