src/Pure/System/ml_process.scala
author wenzelm
Mon, 07 Mar 2016 15:21:50 +0100
changeset 62544 efa178abe023
child 62545 8ebffdaf2ce2
permissions -rw-r--r--
manage the underlying ML process in Scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/ml_process.scala
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     3
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     4
The underlying ML process.
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     5
*/
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     6
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     8
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     9
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    10
object ML_Process
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    11
{
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    12
  def apply(options: Options,
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    13
    heap: String = "",
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    14
    args: List[String] = Nil,
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    15
    process_socket: String = "",
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    16
    secure: Boolean = false,
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    17
    modes: List[String] = Nil): Bash.Process =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    18
  {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    19
    val load_heaps =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    20
    {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    21
      if (heap == "RAW_ML_SYSTEM") Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    22
      else if (heap.iterator.contains('/')) {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    23
        val heap_path = Path.explode(heap)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    24
        if (!heap_path.is_file) error("Bad heap file: " + heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    25
        List(heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    26
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    27
      else {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    28
        val dirs = Isabelle_System.find_logics_dirs()
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    29
        val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    30
        dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    31
          case Some(heap_path) => List(heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    32
          case None =>
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    33
            error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    34
              cat_lines(dirs.map(dir => "  " + dir.implode)))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    35
        }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    36
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    37
    }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    38
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    39
    val eval_heaps =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    40
      load_heaps.map(load_heap =>
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    41
        "PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    42
        " handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    43
        ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    44
        "); OS.Process.exit OS.Process.failure)")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    45
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    46
    val eval_exit =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    47
      if (load_heaps.isEmpty) {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    48
        List(
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    49
          if (Platform.is_windows)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    50
            "fun exit 0 = OS.Process.exit OS.Process.success" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    51
            " | exit 1 = OS.Process.exit OS.Process.failure" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    52
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    53
          else
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    54
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    55
        )
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    56
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    57
      else Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    58
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    59
    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    60
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    61
    val eval_modes =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    62
      if (modes.isEmpty) Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    63
      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    64
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    65
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    66
    // options
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    67
    val isabelle_process_options = Isabelle_System.tmp_file("options")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    68
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    69
    val bash_env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    70
    val eval_options = List("Options.load_default ()")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    71
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    72
    val eval_process =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    73
      if (process_socket == "") Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    74
      else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    75
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    76
    val bash_script =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    77
      """
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    78
        [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    79
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    80
        export ISABELLE_PID="$$"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    81
        export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    82
        mkdir -p "$ISABELLE_TMP"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    83
        chmod $(umask -S) "$ISABELLE_TMP"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    84
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    85
        librarypath "$ML_HOME"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    86
        "$ML_HOME/poly" -q -i $ML_OPTIONS "$@"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    87
        RC="$?"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    88
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    89
        rm -f "$ISABELLE_PROCESS_OPTIONS"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    90
        rmdir "$ISABELLE_TMP"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    91
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    92
        exit "$RC"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    93
      """
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    94
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    95
    val bash_args =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    96
      List("-c", bash_script, "ml_process") :::
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    97
      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    98
        map(eval => List("--eval", eval)).flatten ::: args
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    99
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   100
    Bash.process(null, bash_env, false, bash_args:_*)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   101
  }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   102
}