src/Pure/System/isabelle_process.scala
author wenzelm
Tue Mar 08 11:18:21 2016 +0100 (2016-03-08)
changeset 62555 fd6e64133684
parent 62554 56449c2d20db
child 62556 c115e69f457f
permissions -rw-r--r--
removed pointless option: this is meant for web services using Isabelle/Scala, not command-line tools;
wenzelm@43283
     1
/*  Title:      Pure/System/isabelle_process.scala
wenzelm@27949
     2
    Author:     Makarius
wenzelm@27949
     3
wenzelm@57916
     4
Isabelle process wrapper.
wenzelm@27949
     5
*/
wenzelm@27949
     6
wenzelm@27949
     7
package isabelle
wenzelm@27949
     8
wenzelm@55618
     9
wenzelm@57917
    10
object Isabelle_Process
wenzelm@57917
    11
{
wenzelm@57917
    12
  def apply(
wenzelm@57917
    13
    receiver: Prover.Message => Unit = Console.println(_),
wenzelm@62545
    14
    prover_args: List[String] = Nil): Isabelle_Process =
wenzelm@57917
    15
  {
wenzelm@57917
    16
    val system_channel = System_Channel()
wenzelm@57917
    17
    val system_process =
wenzelm@57916
    18
      try {
wenzelm@62545
    19
        val process =
wenzelm@62548
    20
          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_string(system_channel.server_name) +
wenzelm@62548
    21
            " " + File.bash_args(prover_args))
wenzelm@57916
    22
        process.stdin.close
wenzelm@57916
    23
        process
wenzelm@57916
    24
      }
wenzelm@60215
    25
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
wenzelm@57917
    26
wenzelm@57917
    27
    new Isabelle_Process(receiver, system_channel, system_process)
wenzelm@57917
    28
  }
wenzelm@62554
    29
wenzelm@62554
    30
wenzelm@62554
    31
  /* command line entry point */
wenzelm@62554
    32
wenzelm@62554
    33
  def main(args: Array[String])
wenzelm@62554
    34
  {
wenzelm@62554
    35
    Command_Line.tool {
wenzelm@62554
    36
      var ml_args: List[String] = Nil
wenzelm@62554
    37
      var modes: List[String] = Nil
wenzelm@62554
    38
      var options = Options.init()
wenzelm@62554
    39
wenzelm@62554
    40
      val getopts = Getopts("""
wenzelm@62554
    41
Usage: isabelle_process [OPTIONS] [HEAP]
wenzelm@62554
    42
wenzelm@62554
    43
  Options are:
wenzelm@62554
    44
    -e ML_EXPR   evaluate ML expression on startup
wenzelm@62554
    45
    -f ML_FILE   evaluate ML file on startup
wenzelm@62554
    46
    -m MODE      add print mode for output
wenzelm@62554
    47
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@62554
    48
wenzelm@62554
    49
  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
wenzelm@62554
    50
  $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
wenzelm@62554
    51
  if it is RAW_ML_SYSTEM, the initial ML heap is used.
wenzelm@62554
    52
""",
wenzelm@62554
    53
        "e:" -> (arg => ml_args = ml_args ::: List("--eval", arg)),
wenzelm@62554
    54
        "f:" -> (arg => ml_args = ml_args ::: List("--use", arg)),
wenzelm@62554
    55
        "m:" -> (arg => modes = arg :: modes),
wenzelm@62554
    56
        "o:" -> (arg => options = options + arg))
wenzelm@62554
    57
wenzelm@62554
    58
      val heap =
wenzelm@62554
    59
        getopts(args) match {
wenzelm@62554
    60
          case Nil => ""
wenzelm@62554
    61
          case List(heap) => heap
wenzelm@62554
    62
          case _ => getopts.usage()
wenzelm@62554
    63
        }
wenzelm@62554
    64
wenzelm@62555
    65
      ML_Process(options, heap = heap, args = ml_args, modes = modes).
wenzelm@62554
    66
        result().print_stdout.rc
wenzelm@62554
    67
    }
wenzelm@62554
    68
  }
wenzelm@57916
    69
}
wenzelm@27949
    70
wenzelm@57917
    71
class Isabelle_Process private(
wenzelm@57917
    72
    receiver: Prover.Message => Unit,
wenzelm@57917
    73
    system_channel: System_Channel,
wenzelm@57917
    74
    system_process: Prover.System_Process)
wenzelm@57917
    75
  extends Prover(receiver, system_channel, system_process)
wenzelm@62309
    76
{
wenzelm@62309
    77
  def encode(s: String): String = Symbol.encode(s)
wenzelm@62309
    78
  def decode(s: String): String = Symbol.decode(s)
wenzelm@62309
    79
}