src/Pure/System/isabelle_process.scala
author wenzelm
Tue Mar 08 14:44:11 2016 +0100 (2016-03-08)
changeset 62556 c115e69f457f
parent 62555 fd6e64133684
child 62564 40624a9e94c4
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/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     options: Options,
    14     heap: String = "",
    15     args: List[String] = Nil,
    16     modes: List[String] = Nil,
    17     secure: Boolean = false,
    18     receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
    19   {
    20     val channel = System_Channel()
    21     val process =
    22       try {
    23         ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
    24           process_socket = channel.server_name)
    25       }
    26       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    27     process.stdin.close
    28 
    29     new Isabelle_Process(receiver, channel, process)
    30   }
    31 
    32 
    33   /* command line entry point */
    34 
    35   def main(args: Array[String])
    36   {
    37     Command_Line.tool {
    38       var eval_args: List[String] = Nil
    39       var modes: List[String] = Nil
    40       var options = Options.init()
    41 
    42       val getopts = Getopts("""
    43 Usage: isabelle_process [OPTIONS] [HEAP]
    44 
    45   Options are:
    46     -e ML_EXPR   evaluate ML expression on startup
    47     -f ML_FILE   evaluate ML file on startup
    48     -m MODE      add print mode for output
    49     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    50 
    51   If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
    52   $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
    53   if it is RAW_ML_SYSTEM, the initial ML heap is used.
    54 """,
    55         "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    56         "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    57         "m:" -> (arg => modes = arg :: modes),
    58         "o:" -> (arg => options = options + arg))
    59 
    60       val heap =
    61         getopts(args) match {
    62           case Nil => ""
    63           case List(heap) => heap
    64           case _ => getopts.usage()
    65         }
    66 
    67       ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
    68         result().print_stdout.rc
    69     }
    70   }
    71 }
    72 
    73 class Isabelle_Process private(
    74     receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
    75   extends Prover(receiver, channel, process)
    76 {
    77   def encode(s: String): String = Symbol.encode(s)
    78   def decode(s: String): String = Symbol.decode(s)
    79 }