src/Pure/System/isabelle_process.scala
author wenzelm
Mon Mar 07 20:44:47 2016 +0100 (2016-03-07)
changeset 62548 f8ebb715e06d
parent 62545 8ebffdaf2ce2
child 62554 56449c2d20db
permissions -rw-r--r--
clarified treatment of DEL;
tuned signature;
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@57916
    29
}
wenzelm@27949
    30
wenzelm@57917
    31
class Isabelle_Process private(
wenzelm@57917
    32
    receiver: Prover.Message => Unit,
wenzelm@57917
    33
    system_channel: System_Channel,
wenzelm@57917
    34
    system_process: Prover.System_Process)
wenzelm@57917
    35
  extends Prover(receiver, system_channel, system_process)
wenzelm@62309
    36
{
wenzelm@62309
    37
  def encode(s: String): String = Symbol.encode(s)
wenzelm@62309
    38
  def decode(s: String): String = Symbol.decode(s)
wenzelm@62309
    39
}