src/Pure/ML/ml_process.scala
author wenzelm
Sun Oct 08 12:36:00 2017 +0200 (21 months ago)
changeset 66781 dac4cfbfede8
parent 66717 67dbf5cdc056
child 66782 193c31b79a33
permissions -rw-r--r--
proper output of raw ML;
     1 /*  Title:      Pure/ML/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_string0, ML_Syntax.print_string0))(table)
   102           def print_list(list: List[String]): String =
   103             ML_Syntax.print_list(ML_Syntax.print_string0)(list)
   104           List("Resources.init_session_base" +
   105             " {global_theories = " + print_table(base.global_theories.toList) +
   106             ", loaded_theories = " + print_list(base.loaded_theories.keys) +
   107             ", known_theories = " + print_table(base.dest_known_theories) + "}")
   108       }
   109 
   110     // process
   111     val eval_process =
   112       if (heaps.isEmpty)
   113         List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
   114       else
   115         channel match {
   116           case None =>
   117             List("Isabelle_Process.init_options ()")
   118           case Some(ch) =>
   119             List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
   120         }
   121 
   122     // ISABELLE_TMP
   123     val isabelle_tmp = Isabelle_System.tmp_dir("process")
   124     val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
   125 
   126     val ml_runtime_options =
   127     {
   128       val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
   129       if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
   130       else ml_options ::: List("--gcthreads", options.int("threads").toString)
   131     }
   132 
   133     // bash
   134     val bash_args =
   135       ml_runtime_options :::
   136       (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
   137         map(eval => List("--eval", eval)).flatten ::: args
   138 
   139     Bash.process(
   140       "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
   141         Bash.strings(bash_args),
   142       cwd = cwd,
   143       env =
   144         Isabelle_System.library_path(env ++ env_options ++ env_tmp,
   145           Isabelle_System.getenv_strict("ML_HOME")),
   146       redirect = redirect,
   147       cleanup = () =>
   148         {
   149           isabelle_process_options.delete
   150           Isabelle_System.rm_tree(isabelle_tmp)
   151           cleanup()
   152         })
   153   }
   154 
   155 
   156   /* Isabelle tool wrapper */
   157 
   158   val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
   159   {
   160     var dirs: List[Path] = Nil
   161     var eval_args: List[String] = Nil
   162     var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   163     var modes: List[String] = Nil
   164     var options = Options.init()
   165 
   166     val getopts = Getopts("""
   167 Usage: isabelle process [OPTIONS]
   168 
   169   Options are:
   170     -T THEORY    load theory
   171     -d DIR       include session directory
   172     -e ML_EXPR   evaluate ML expression on startup
   173     -f ML_FILE   evaluate ML file on startup
   174     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   175     -m MODE      add print mode for output
   176     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   177 
   178   Run the raw Isabelle ML process in batch mode.
   179 """,
   180       "T:" -> (arg =>
   181         eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
   182       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   183       "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
   184       "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
   185       "l:" -> (arg => logic = arg),
   186       "m:" -> (arg => modes = arg :: modes),
   187       "o:" -> (arg => options = options + arg))
   188 
   189     val more_args = getopts(args)
   190     if (args.isEmpty || !more_args.isEmpty) getopts.usage()
   191 
   192     val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
   193       result().print_stdout.rc
   194     sys.exit(rc)
   195   })
   196 }