src/Pure/System/isabelle_process.scala
author wenzelm
Tue, 12 Aug 2014 18:36:43 +0200
changeset 57916 2c2c24dbf0a4
parent 57915 448325de6e4f
child 57917 8ce97e5d545f
permissions -rw-r--r--
generic process wrapping in Prover; clarified module arrangement;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43283
446e6621762d updated headers;
wenzelm
parents: 40848
diff changeset
     1
/*  Title:      Pure/System/isabelle_process.scala
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     3
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
     4
Isabelle process wrapper.
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     5
*/
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     6
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     7
package isabelle
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     8
55618
995162143ef4 tuned imports;
wenzelm
parents: 54443
diff changeset
     9
45055
55274f7e306b explicit option for socket vs. fifo communication;
wenzelm
parents: 45027
diff changeset
    10
class Isabelle_Process(
56831
e3ccf0809d51 prefer scala.Console with its support for thread-local redirection;
wenzelm
parents: 56794
diff changeset
    11
  receiver: Prover.Message => Unit = Console.println(_),
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    12
  prover_args: List[String] = Nil) extends Prover(receiver,
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    13
    {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    14
      val system_channel = System_Channel()
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    15
      try {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    16
        val cmdline =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    17
          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    18
            (system_channel.prover_args ::: prover_args)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    19
        val process =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    20
          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    21
            Prover.System_Process { def channel = system_channel }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    22
        process.stdin.close
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    23
        process
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    24
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    25
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    26
    })
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
    27
{
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    28
  def encode(s: String): String = Symbol.encode(s)
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    29
  def decode(s: String): String = Symbol.decode(s)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    30
}
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    31