src/Pure/System/isabelle_process.scala
author wenzelm
Sun May 03 00:01:10 2015 +0200 (2015-05-03)
changeset 60215 5fb4990dfc73
parent 57917 8ce97e5d545f
child 60991 2fc5a44346b5
permissions -rw-r--r--
misc tuning, based on warnings by IntelliJ IDEA;
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@57917
    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@57916
    19
        val cmdline =
wenzelm@57916
    20
          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
wenzelm@57916
    21
            (system_channel.prover_args ::: prover_args)
wenzelm@57916
    22
        val process =
wenzelm@57916
    23
          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
wenzelm@57917
    24
            Prover.System_Process
wenzelm@57916
    25
        process.stdin.close
wenzelm@57916
    26
        process
wenzelm@57916
    27
      }
wenzelm@60215
    28
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
wenzelm@57917
    29
wenzelm@57917
    30
    new Isabelle_Process(receiver, system_channel, system_process)
wenzelm@57917
    31
  }
wenzelm@57916
    32
}
wenzelm@27949
    33
wenzelm@57917
    34
class Isabelle_Process private(
wenzelm@57917
    35
    receiver: Prover.Message => Unit,
wenzelm@57917
    36
    system_channel: System_Channel,
wenzelm@57917
    37
    system_process: Prover.System_Process)
wenzelm@57917
    38
  extends Prover(receiver, system_channel, system_process)
wenzelm@57917
    39
  {
wenzelm@57917
    40
    def encode(s: String): String = Symbol.encode(s)
wenzelm@57917
    41
    def decode(s: String): String = Symbol.decode(s)
wenzelm@57917
    42
  }
wenzelm@57917
    43