src/Pure/System/isabelle_process.scala
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 62754 c35012b86e6f
child 65216 060a8a1f2dec
permissions -rw-r--r--
clarified mode of ROOT.ML files;
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,
62754
c35012b86e6f proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
wenzelm
parents: 62668
diff changeset
    16
    dirs: List[Path] = Nil,
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    17
    modes: List[String] = Nil,
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62586
diff changeset
    18
    receiver: Prover.Receiver = Console.println(_),
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62586
diff changeset
    19
    store: Sessions.Store = Sessions.store()): Isabelle_Process =
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    20
  {
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    21
    val channel = System_Channel()
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    22
    val process =
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    23
      try {
62754
c35012b86e6f proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
wenzelm
parents: 62668
diff changeset
    24
        ML_Process(options, logic = logic, args = args, dirs = dirs,
c35012b86e6f proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
wenzelm
parents: 62668
diff changeset
    25
          modes = modes, store = store, channel = Some(channel))
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    26
      }
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    27
      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    28
    process.stdin.close
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    29
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    30
    new Isabelle_Process(receiver, channel, process)
57917
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(
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    35
    receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62555
diff changeset
    36
  extends Prover(receiver, channel, process)
62309
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    37
{
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    38
  def encode(s: String): String = Symbol.encode(s)
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    39
  def decode(s: String): String = Symbol.decode(s)
96c9a259d275 tuned whitespace;
wenzelm
parents: 62308
diff changeset
    40
}