src/Pure/System/isabelle_process.scala
author immler
Tue, 22 Dec 2015 21:58:27 +0100
changeset 61915 e9812a95d108
parent 60991 2fc5a44346b5
child 62296 b04a5ddd6121
permissions -rw-r--r--
theory for type of bounded linear functions; differentiation under the integral sign

/*  Title:      Pure/System/isabelle_process.scala
    Author:     Makarius

Isabelle process wrapper.
*/

package isabelle


object Isabelle_Process
{
  def apply(
    receiver: Prover.Message => Unit = Console.println(_),
    prover_args: List[String] = Nil): Isabelle_Process =
  {
    val system_channel = System_Channel()
    val system_process =
      try {
        val cmdline =
          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
            (system_channel.prover_args ::: prover_args)
        val process = Bash.process(null, null, false, cmdline: _*)
        process.stdin.close
        process
      }
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }

    new Isabelle_Process(receiver, system_channel, system_process)
  }
}

class Isabelle_Process private(
    receiver: Prover.Message => Unit,
    system_channel: System_Channel,
    system_process: Prover.System_Process)
  extends Prover(receiver, system_channel, system_process)
  {
    def encode(s: String): String = Symbol.encode(s)
    def decode(s: String): String = Symbol.decode(s)
  }