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