src/Pure/System/isabelle_process.scala
author wenzelm
Fri, 18 Mar 2016 17:58:19 +0100
changeset 62668 360d3464919c
parent 62634 aa3b47b32100
child 62754 c35012b86e6f
permissions -rw-r--r--
discontinued slightly odd "secure" mode;
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(
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    13
    options: Options,
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    14
    logic: String = "",
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    15
    args: List[String] = Nil,
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    16
    modes: List[String] = Nil,
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62586
diff changeset
    17
    receiver: Prover.Receiver = Console.println(_),
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62586
diff changeset
    18
    store: Sessions.Store = Sessions.store()): Isabelle_Process =
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    19
  {
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    20
    val channel = System_Channel()
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    21
    val process =
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    22
      try {
62668
360d3464919c discontinued slightly odd "secure" mode;
wenzelm
parents: 62634
diff changeset
    23
        ML_Process(options, logic = logic, args = args, modes = modes, store = store,
360d3464919c discontinued slightly odd "secure" mode;
wenzelm
parents: 62634
diff changeset
    24
          channel = Some(channel))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    25
      }
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    26
      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    27
    process.stdin.close
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    28
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    29
    new Isabelle_Process(receiver, channel, process)
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    30
  }
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    31
}
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    32
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    33
class Isabelle_Process private(
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    34
    receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    35
  extends Prover(receiver, channel, process)
62309
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    36
{
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    37
  def encode(s: String): String = Symbol.encode(s)
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    38
  def decode(s: String): String = Symbol.decode(s)
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    39
}