src/Pure/System/isabelle_process.scala
author wenzelm
Sat, 13 Feb 2016 20:41:56 +0100
changeset 62296 b04a5ddd6121
parent 60991 2fc5a44346b5
child 62299 9e95a4afb8c3
permissions -rw-r--r--
clarified bash process -- similar to ML version;
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(_),
62296
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 60991
diff changeset
    14
    prover_args: String = ""): Isabelle_Process =
57917
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 {
62296
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 60991
diff changeset
    19
        val script =
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 60991
diff changeset
    20
          "\"$ISABELLE_PROCESS\" " + system_channel.prover_options +
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 60991
diff changeset
    21
            (if (prover_args == "") "" else " " + prover_args)
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 60991
diff changeset
    22
        val process = Bash.process(null, null, false, "-c", script)
57916
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    23
        process.stdin.close
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    24
        process
2c2c24dbf0a4 generic process wrapping in Prover;
wenzelm
parents: 57915
diff changeset
    25
      }
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 57917
diff changeset
    26
      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    27
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    28
    new Isabelle_Process(receiver, system_channel, system_process)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    29
  }
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
57917
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    32
class Isabelle_Process private(
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    33
    receiver: Prover.Message => Unit,
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    34
    system_channel: System_Channel,
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    35
    system_process: Prover.System_Process)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    36
  extends Prover(receiver, system_channel, system_process)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    37
  {
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    38
    def encode(s: String): String = Symbol.encode(s)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    39
    def decode(s: String): String = Symbol.decode(s)
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    40
  }
8ce97e5d545f tuned signature;
wenzelm
parents: 57916
diff changeset
    41