src/Pure/Tools/ml_process.scala
author wenzelm
Wed Apr 12 22:32:55 2017 +0200 (2017-04-12 ago)
changeset 65471 05e5bffcf1d8
parent 65457 2bf0d2fcd506
permissions -rw-r--r--
clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;
     1 /*  Title:      Pure/Tools/ml_process.scala
     2     Author:     Makarius
     3 
     4 The raw ML process.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 
    13 object 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     channel: Option[System_Channel] = None,
    26     sessions: Option[Sessions.T] = None,
    27     session_base: Option[Sessions.Base] = None,
    28     store: Sessions.Store = Sessions.store()): Bash.Process =
    29   {
    30     val logic_name = Isabelle_System.default_logic(logic)
    31     val heaps: List[String] =
    32       if (raw_ml_system) Nil
    33       else {
    34         val selection = Sessions.Selection(sessions = List(logic_name))
    35         val (_, selected_sessions) =
    36           sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
    37         (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
    38           map(a => File.platform_path(store.heap(a)))
    39       }
    40 
    41     val eval_init =
    42       if (heaps.isEmpty) {
    43         List(
    44           """
    45           fun chapter (_: string) = ();
    46           fun section (_: string) = ();
    47           fun subsection (_: string) = ();
    48           fun subsubsection (_: string) = ();
    49           fun paragraph (_: string) = ();
    50           fun subparagraph (_: string) = ();
    51           val ML_file = PolyML.use;
    52           """,
    53           if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
    54             """
    55               structure FixedInt = IntInf;
    56               structure RunCall =
    57               struct
    58                 open RunCall
    59                 val loadWord: word * word -> word =
    60                   run_call2 RuntimeCalls.POLY_SYS_load_word;
    61                 val storeWord: word * word * word -> unit =
    62                   run_call3 RuntimeCalls.POLY_SYS_assign_word;
    63               end;
    64             """
    65           else "",
    66           if (Platform.is_windows)
    67             "fun exit 0 = OS.Process.exit OS.Process.success" +
    68             " | exit 1 = OS.Process.exit OS.Process.failure" +
    69             " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
    70           else
    71             "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
    72           "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
    73           "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
    74       }
    75       else
    76         List(
    77           "(PolyML.SaveState.loadHierarchy " +
    78             ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
    79           "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
    80           ML_Syntax.print_string0(": " + logic_name + "\n") +
    81           "); OS.Process.exit OS.Process.failure)")
    82 
    83     val eval_modes =
    84       if (modes.isEmpty) Nil
    85       else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
    86 
    87     // options
    88     val isabelle_process_options = Isabelle_System.tmp_file("options")
    89     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
    90     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    91     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
    92 
    93     // session base
    94     val eval_session_base =
    95       session_base match {
    96         case None => Nil
    97         case Some(base) =>
    98           def print_table(table: List[(String, String)]): String =
    99             ML_Syntax.print_list(
   100               ML_Syntax.print_pair(
   101                 ML_Syntax.print_string, ML_Syntax.print_string))(table)
   102           List("Resources.set_session_base {default_qualifier = \"\"" +
   103             ", global_theories = " + print_table(base.global_theories.toList) +
   104             ", loaded_theories = " + print_table(base.loaded_theories.toList) +
   105             ", known_theories = " + print_table(base.dest_known_theories) + "}")
   106       }
   107 
   108     // process
   109     val eval_process =
   110       if (heaps.isEmpty)
   111         List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
   112       else
   113         channel match {
   114           case None =>
   115             List("Isabelle_Process.init_options ()")
   116           case Some(ch) =>
   117             List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
   118         }
   119 
   120     // ISABELLE_TMP
   121     val isabelle_tmp = Isabelle_System.tmp_dir("process")
   122     val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
   123 
   124     val ml_runtime_options =
   125     {
   126       val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
   127       if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
   128       else ml_options ::: List("--gcthreads", options.int("threads").toString)
   129     }
   130 
   131     // bash
   132     val bash_args =
   133       ml_runtime_options :::
   134       (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
   135         map(eval => List("--eval", eval)).flatten ::: args
   136 
   137     Bash.process(
   138       "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
   139         Bash.strings(bash_args),
   140       cwd = cwd,
   141       env =
   142         Isabelle_System.library_path(env ++ env_options ++ env_tmp,
   143           Isabelle_System.getenv_strict("ML_HOME")),
   144       redirect = redirect,
   145       cleanup = () =>
   146         {
   147           isabelle_process_options.delete
   148           Isabelle_System.rm_tree(isabelle_tmp)
   149           cleanup()
   150         })
   151   }
   152 
   153 
   154   /* Isabelle tool wrapper */
   155 
   156   val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
   157   {
   158     var dirs: List[Path] = Nil
   159     var eval_args: List[String] = Nil
   160     var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   161     var modes: List[String] = Nil
   162     var options = Options.init()
   163 
   164     val getopts = Getopts("""
   165 Usage: isabelle process [OPTIONS]
   166 
   167   Options are:
   168     -T THEORY    load theory
   169     -d DIR       include session directory
   170     -e ML_EXPR   evaluate ML expression on startup
   171     -f ML_FILE   evaluate ML file on startup
   172     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   173     -m MODE      add print mode for output
   174     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   175 
   176   Run the raw Isabelle ML process in batch mode.
   177 """,
   178       "T:" -> (arg =>
   179         eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
   180       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   181       "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
   182       "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
   183       "l:" -> (arg => logic = arg),
   184       "m:" -> (arg => modes = arg :: modes),
   185       "o:" -> (arg => options = options + arg))
   186 
   187     val more_args = getopts(args)
   188     if (args.isEmpty || !more_args.isEmpty) getopts.usage()
   189 
   190     val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
   191       result().print_stdout.rc
   192     sys.exit(rc)
   193   })
   194 }