src/Pure/System/ml_process.scala
author wenzelm
Tue Mar 08 14:44:11 2016 +0100 (2016-03-08)
changeset 62556 c115e69f457f
parent 62548 f8ebb715e06d
child 62557 a4ea3a222e0e
permissions -rw-r--r--
more abstract Session.start, without prover command-line;
Isabelle_Process.apply is directly based on ML_Process;
clarified Isabelle_Process.main command-line;
tuned signature;
     1 /*  Title:      Pure/System/ml_process.scala
     2     Author:     Makarius
     3 
     4 The underlying ML process.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object ML_Process
    11 {
    12   def apply(options: Options,
    13     heap: String = "",
    14     args: List[String] = Nil,
    15     modes: List[String] = Nil,
    16     secure: Boolean = false,
    17     process_socket: String = ""): Bash.Process =
    18   {
    19     val load_heaps =
    20     {
    21       if (heap == "RAW_ML_SYSTEM") Nil
    22       else if (heap.iterator.contains('/')) {
    23         val heap_path = Path.explode(heap)
    24         if (!heap_path.is_file) error("Bad heap file: " + heap_path)
    25         List(heap_path)
    26       }
    27       else {
    28         val dirs = Isabelle_System.find_logics_dirs()
    29         val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
    30         dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
    31           case Some(heap_path) => List(heap_path)
    32           case None =>
    33             error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
    34               cat_lines(dirs.map(dir => "  " + dir.implode)))
    35         }
    36       }
    37     }
    38 
    39     val eval_heaps =
    40       load_heaps.map(load_heap =>
    41         "PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
    42         " handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
    43         ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
    44         "); OS.Process.exit OS.Process.failure)")
    45 
    46     val eval_exit =
    47       if (load_heaps.isEmpty) {
    48         List(
    49           if (Platform.is_windows)
    50             "fun exit 0 = OS.Process.exit OS.Process.success" +
    51             " | exit 1 = OS.Process.exit OS.Process.failure" +
    52             " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
    53           else "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
    54           "PolyML.print_depth 10")
    55       }
    56       else Nil
    57 
    58     val eval_modes =
    59       if (modes.isEmpty) Nil
    60       else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(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 = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    66     val eval_options = if (load_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 (process_socket == "") Nil
    72       else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
    73 
    74     // bash
    75     val bash_args =
    76       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
    77       (eval_heaps ::: eval_exit ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
    78         map(eval => List("--eval", eval)).flatten ::: args
    79 
    80     Bash.process(env = env, script =
    81       """
    82         [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
    83 
    84         export ISABELLE_PID="$$"
    85         export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
    86         mkdir -p "$ISABELLE_TMP"
    87         chmod $(umask -S) "$ISABELLE_TMP"
    88 
    89         librarypath "$ML_HOME"
    90         "$ML_HOME/poly" -q -i """ + File.bash_args(bash_args) + """
    91         RC="$?"
    92 
    93         rm -f "$ISABELLE_PROCESS_OPTIONS"
    94         rmdir "$ISABELLE_TMP"
    95 
    96         exit "$RC"
    97       """)
    98   }
    99 }