src/Pure/System/isabelle_process.scala
author wenzelm
Tue Aug 12 18:36:43 2014 +0200 (2014-08-12)
changeset 57916 2c2c24dbf0a4
parent 57915 448325de6e4f
child 57917 8ce97e5d545f
permissions -rw-r--r--
generic process wrapping in Prover;
clarified module arrangement;
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@45055
    10
class Isabelle_Process(
wenzelm@56831
    11
  receiver: Prover.Message => Unit = Console.println(_),
wenzelm@57916
    12
  prover_args: List[String] = Nil) extends Prover(receiver,
wenzelm@57916
    13
    {
wenzelm@57916
    14
      val system_channel = System_Channel()
wenzelm@57916
    15
      try {
wenzelm@57916
    16
        val cmdline =
wenzelm@57916
    17
          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
wenzelm@57916
    18
            (system_channel.prover_args ::: prover_args)
wenzelm@57916
    19
        val process =
wenzelm@57916
    20
          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
wenzelm@57916
    21
            Prover.System_Process { def channel = system_channel }
wenzelm@57916
    22
        process.stdin.close
wenzelm@57916
    23
        process
wenzelm@57916
    24
      }
wenzelm@57916
    25
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
wenzelm@57916
    26
    })
wenzelm@29192
    27
{
wenzelm@48705
    28
  def encode(s: String): String = Symbol.encode(s)
wenzelm@48705
    29
  def decode(s: String): String = Symbol.decode(s)
wenzelm@57916
    30
}
wenzelm@27949
    31