src/Pure/Tools/ml_process.scala
author wenzelm
Wed Mar 16 20:50:38 2016 +0100 (2016-03-16)
changeset 62638 751cf9f3d433
parent 62637 0189fe0f6452
child 62639 699e86051e35
permissions -rw-r--r--
tuned signature;
     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     secure: 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     tree: Option[Sessions.Tree] = None,
    27     store: Sessions.Store = Sessions.store()): Bash.Process =
    28   {
    29     val logic_name = Isabelle_System.default_logic(logic)
    30     val heaps: List[String] =
    31       if (logic_name == "RAW_ML_SYSTEM") Nil
    32       else {
    33         val session_tree = tree.getOrElse(Sessions.load(options, dirs))
    34         (session_tree.ancestors(logic_name) ::: List(logic_name)).
    35           map(a => File.platform_path(store.heap(a)))
    36       }
    37 
    38     val eval_init =
    39       if (heaps.isEmpty) {
    40         List(
    41           if (Platform.is_windows)
    42             "fun exit 0 = OS.Process.exit OS.Process.success" +
    43             " | exit 1 = OS.Process.exit OS.Process.failure" +
    44             " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
    45           else
    46             "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
    47           "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
    48           "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
    49       }
    50       else
    51         List(
    52           "(PolyML.SaveState.loadHierarchy " +
    53             ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
    54           "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
    55           ML_Syntax.print_string0(": " + logic_name + "\n") +
    56           "); OS.Process.exit OS.Process.failure)")
    57 
    58     val eval_modes =
    59       if (modes.isEmpty) Nil
    60       else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
    61 
    62     // options
    63     val isabelle_process_options = Isabelle_System.tmp_file("options")
    64     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
    65     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    66     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
    67 
    68     val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
    69 
    70     val eval_process =
    71       if (heaps.isEmpty)
    72         List("PolyML.print_depth 10")
    73       else
    74         channel match {
    75           case None =>
    76             List("(default_print_depth 10; Isabelle_Process.init_options ())")
    77           case Some(ch) =>
    78             List("(default_print_depth 10; Isabelle_Process.init_protocol " +
    79               ML_Syntax.print_string0(ch.server_name) + ")")
    80         }
    81 
    82     // ISABELLE_TMP
    83     val isabelle_tmp = Isabelle_System.tmp_dir("process")
    84     val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
    85 
    86     // bash
    87     val bash_args =
    88       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    89       (eval_init ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
    90         map(eval => List("--eval", eval)).flatten ::: args
    91 
    92     Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
    93       cwd = cwd,
    94       env =
    95         Isabelle_System.library_path(env ++ env_options ++ env_tmp,
    96           Isabelle_System.getenv_strict("ML_HOME")),
    97       redirect = redirect,
    98       cleanup = () =>
    99         {
   100           isabelle_process_options.delete
   101           Isabelle_System.rm_tree(isabelle_tmp)
   102           cleanup()
   103         })
   104   }
   105 
   106 
   107   /* command line entry point */
   108 
   109   def main(args: Array[String])
   110   {
   111     Command_Line.tool {
   112       var eval_args: List[String] = Nil
   113       var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   114       var modes: List[String] = Nil
   115       var options = Options.init()
   116 
   117       val getopts = Getopts("""
   118 Usage: isabelle process [OPTIONS]
   119 
   120   Options are:
   121     -e ML_EXPR   evaluate ML expression on startup
   122     -f ML_FILE   evaluate ML file on startup
   123     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   124     -m MODE      add print mode for output
   125     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   126 
   127   Run the raw Isabelle ML process in batch mode.
   128 """,
   129         "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
   130         "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
   131         "l:" -> (arg => logic = arg),
   132         "m:" -> (arg => modes = arg :: modes),
   133         "o:" -> (arg => options = options + arg))
   134 
   135       val more_args = getopts(args)
   136       if (args.isEmpty || !more_args.isEmpty) getopts.usage()
   137 
   138       ML_Process(options, logic = logic, args = eval_args ::: args.toList, modes = modes).
   139         result().print_stdout.rc
   140     }
   141   }
   142 }