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