src/Pure/System/isabelle_process.scala
author wenzelm
Tue, 12 Aug 2014 18:54:53 +0200
changeset 57917 8ce97e5d545f
parent 57916 2c2c24dbf0a4
child 60215 5fb4990dfc73
permissions -rw-r--r--
tuned signature;
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
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    10
object Isabelle_Process
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    11
{
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    12
  def apply(
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    13
    receiver: Prover.Message => Unit = Console.println(_),
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    14
    prover_args: List[String] = Nil): Isabelle_Process =
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    15
  {
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    16
    val system_channel = System_Channel()
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    17
    val system_process =
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    18
      try {
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    19
        val cmdline =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    20
          Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    21
            (system_channel.prover_args ::: prover_args)
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    22
        val process =
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    23
          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    24
            Prover.System_Process
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    25
        process.stdin.close
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    26
        process
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    27
      }
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    28
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    29
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    30
    new Isabelle_Process(receiver, system_channel, system_process)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    31
  }
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    32
}
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    33
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    34
class Isabelle_Process private(
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    35
    receiver: Prover.Message => Unit,
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    36
    system_channel: System_Channel,
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    37
    system_process: Prover.System_Process)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    38
  extends Prover(receiver, system_channel, system_process)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    39
  {
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    40
    def encode(s: String): String = Symbol.encode(s)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    41
    def decode(s: String): String = Symbol.decode(s)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    42
  }
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    43