src/Pure/System/isabelle_process.scala
author wenzelm
Thu, 17 Dec 2009 20:14:00 +0100
changeset 34100 ea24958c2af5
parent 32474 0818e6b1c8a6
child 34109 f49d45afa634
permissions -rw-r--r--
fifo: raw byte stream; Result: fully decoded symbols and tree structure; adapted to simplified message format; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29648
diff changeset
     1
/*  Title:      Pure/System/isabelle_process.ML
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
     3
    Options:    :folding=explicit:collapseFolds=1:
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     4
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     5
Isabelle process management -- always reactive due to multi-threaded I/O.
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
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     8
package isabelle
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     9
27955
4c32c5e75eca use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents: 27949
diff changeset
    10
import java.util.concurrent.LinkedBlockingQueue
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
    11
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
28056
18dbe34f6c5d moved charset to isabelle_system.scala;
wenzelm
parents: 28045
diff changeset
    12
  InputStream, OutputStream, IOException}
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    13
32474
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    14
import scala.actors.Actor
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    15
import Actor._
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    16
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    17
32474
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    18
object Isabelle_Process
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    19
{
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    20
  /* results */
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    21
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    22
  object Kind extends Enumeration {
28344
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    23
    //{{{ values and codes
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    24
    // internal system notification
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    25
    val SYSTEM = Value("SYSTEM")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    26
    // Posix channels/events
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    27
    val STDIN = Value("STDIN")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    28
    val STDOUT = Value("STDOUT")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    29
    val SIGNAL = Value("SIGNAL")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    30
    val EXIT = Value("EXIT")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    31
    // Isabelle messages
28344
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    32
    val INIT = Value("INIT")
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    33
    val STATUS = Value("STATUS")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    34
    val WRITELN = Value("WRITELN")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    35
    val PRIORITY = Value("PRIORITY")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    36
    val TRACING = Value("TRACING")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    37
    val WARNING = Value("WARNING")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    38
    val ERROR = Value("ERROR")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    39
    val DEBUG = Value("DEBUG")
28344
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    40
    // messages codes
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    41
    val code = Map(
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    42
      ('A' : Int) -> Kind.INIT,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    43
      ('B' : Int) -> Kind.STATUS,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    44
      ('C' : Int) -> Kind.WRITELN,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    45
      ('D' : Int) -> Kind.PRIORITY,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    46
      ('E' : Int) -> Kind.TRACING,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    47
      ('F' : Int) -> Kind.WARNING,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    48
      ('G' : Int) -> Kind.ERROR,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    49
      ('H' : Int) -> Kind.DEBUG,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    50
      ('0' : Int) -> Kind.SYSTEM,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    51
      ('1' : Int) -> Kind.STDIN,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    52
      ('2' : Int) -> Kind.STDOUT,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    53
      ('3' : Int) -> Kind.SIGNAL,
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    54
      ('4' : Int) -> Kind.EXIT)
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    55
    // message markup
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    56
    val markup = Map(
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    57
      Kind.INIT -> Markup.INIT,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    58
      Kind.STATUS -> Markup.STATUS,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    59
      Kind.WRITELN -> Markup.WRITELN,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    60
      Kind.PRIORITY -> Markup.PRIORITY,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    61
      Kind.TRACING -> Markup.TRACING,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    62
      Kind.WARNING -> Markup.WARNING,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    63
      Kind.ERROR -> Markup.ERROR,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    64
      Kind.DEBUG -> Markup.DEBUG,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    65
      Kind.SYSTEM -> Markup.SYSTEM,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    66
      Kind.STDIN -> Markup.STDIN,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    67
      Kind.STDOUT -> Markup.STDOUT,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    68
      Kind.SIGNAL -> Markup.SIGNAL,
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    69
      Kind.EXIT -> Markup.EXIT)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    70
    //}}}
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    71
    def is_raw(kind: Value) =
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
    72
      kind == STDOUT
27990
f9dd4c9ed812 Kind: added is_control;
wenzelm
parents: 27973
diff changeset
    73
    def is_control(kind: Value) =
28344
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    74
      kind == SYSTEM ||
27990
f9dd4c9ed812 Kind: added is_control;
wenzelm
parents: 27973
diff changeset
    75
      kind == SIGNAL ||
28344
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    76
      kind == EXIT
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    77
    def is_system(kind: Value) =
28344
f4a17868bde5 protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents: 28303
diff changeset
    78
      kind == SYSTEM ||
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    79
      kind == STDIN ||
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    80
      kind == SIGNAL ||
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    81
      kind == EXIT ||
28498
cb1b43edb5ed eliminated prompt messages;
wenzelm
parents: 28497
diff changeset
    82
      kind == STATUS
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    83
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    84
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    85
  class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    86
  {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    87
    def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    88
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    89
    override def toString: String =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    90
    {
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    91
      val res =
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    92
        if (kind == Kind.STATUS) body.map(_.toString).mkString
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    93
        else body.map(XML.content(_).mkString).mkString
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    94
      if (props.isEmpty)
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    95
        kind.toString + " [[" + res + "]]"
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    96
      else
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    97
        kind.toString + " " +
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    98
          (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    99
    }
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   100
    def is_raw = Kind.is_raw(kind)
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   101
    def is_control = Kind.is_control(kind)
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   102
    def is_system = Kind.is_system(kind)
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   103
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   104
}
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   105
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   106
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   107
class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*)
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   108
{
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31498
diff changeset
   109
  import Isabelle_Process._
29194
wenzelm
parents: 29192
diff changeset
   110
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   111
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   112
  /* demo constructor */
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   113
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   114
  def this(args: String*) =
32474
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
   115
    this(new Isabelle_System,
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
   116
      new Actor { def act = loop { react { case res => Console.println(res) } } }.start, args: _*)
29174
d4058295affb proper class IsabelleSystem -- no longer static;
wenzelm
parents: 29140
diff changeset
   117
d4058295affb proper class IsabelleSystem -- no longer static;
wenzelm
parents: 29140
diff changeset
   118
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   119
  /* process information */
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   120
29648
ead544f3d6a1 annotate shared vars as @volatile;
wenzelm
parents: 29573
diff changeset
   121
  @volatile private var proc: Process = null
ead544f3d6a1 annotate shared vars as @volatile;
wenzelm
parents: 29573
diff changeset
   122
  @volatile private var closing = false
ead544f3d6a1 annotate shared vars as @volatile;
wenzelm
parents: 29573
diff changeset
   123
  @volatile private var pid: String = null
ead544f3d6a1 annotate shared vars as @volatile;
wenzelm
parents: 29573
diff changeset
   124
  @volatile private var the_session: String = null
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   125
  def session = the_session
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   126
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   127
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   128
  /* results */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   129
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   130
  private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   131
  {
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   132
    if (kind == Kind.INIT) {
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   133
      val map = Map(props: _*)
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   134
      if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   135
      if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   136
    }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   137
    receiver ! new Result(kind, props, body)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   138
  }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   139
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   140
  private def put_result(kind: Kind.Value, text: String)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   141
  {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   142
    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
27992
131f7ea9e6e6 added try_result;
wenzelm
parents: 27990
diff changeset
   143
  }
131f7ea9e6e6 added try_result;
wenzelm
parents: 27990
diff changeset
   144
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   145
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   146
  /* signals */
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   147
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   148
  def interrupt() = synchronized {
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   149
    if (proc == null) error("Cannot interrupt Isabelle: no process")
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   150
    if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid")
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   151
    else {
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   152
      try {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   153
        if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   154
          put_result(Kind.SIGNAL, "INT")
27990
f9dd4c9ed812 Kind: added is_control;
wenzelm
parents: 27973
diff changeset
   155
        else
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   156
          put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed")
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   157
      }
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   158
      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   159
    }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   160
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   161
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   162
  def kill() = synchronized {
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   163
    if (proc == 0) error("Cannot kill Isabelle: no process")
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   164
    else {
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   165
      try_close()
27990
f9dd4c9ed812 Kind: added is_control;
wenzelm
parents: 27973
diff changeset
   166
      Thread.sleep(500)
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   167
      put_result(Kind.SIGNAL, "KILL")
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   168
      proc.destroy
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   169
      proc = null
27990
f9dd4c9ed812 Kind: added is_control;
wenzelm
parents: 27973
diff changeset
   170
      pid = null
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   171
    }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   172
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   173
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   174
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   175
  /* output being piped into the process */
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   176
27990
f9dd4c9ed812 Kind: added is_control;
wenzelm
parents: 27973
diff changeset
   177
  private val output = new LinkedBlockingQueue[String]
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   178
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   179
  private def output_raw(text: String) = synchronized {
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   180
    if (proc == null) error("Cannot output to Isabelle: no process")
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   181
    if (closing) error("Cannot output to Isabelle: already closing")
27955
4c32c5e75eca use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents: 27949
diff changeset
   182
    output.put(text)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   183
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   184
28303
8c4a4f256c16 output_sync is now public;
wenzelm
parents: 28063
diff changeset
   185
  def output_sync(text: String) =
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   186
    output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   187
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   188
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   189
  def command(text: String) =
32448
a89f876731c5 moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents: 31797
diff changeset
   190
    output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   191
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   192
  def command(props: List[(String, String)], text: String) =
32448
a89f876731c5 moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents: 31797
diff changeset
   193
    output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
a89f876731c5 moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents: 31797
diff changeset
   194
      Isabelle_Syntax.encode_string(text))
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   195
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   196
  def ML(text: String) =
32448
a89f876731c5 moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents: 31797
diff changeset
   197
    output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   198
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   199
  def close() = synchronized {    // FIXME watchdog/timeout
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   200
    output_raw("\u0000")
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   201
    closing = true
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   202
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   203
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   204
  def try_close() = synchronized {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   205
    if (proc != null && !closing) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   206
      try { close() }
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   207
      catch { case _: RuntimeException => }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   208
    }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   209
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   210
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   211
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   212
  /* stdin */
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   213
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   214
  private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   215
    override def run() = {
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31498
diff changeset
   216
      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Isabelle_System.charset))
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   217
      var finished = false
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   218
      while (!finished) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   219
        try {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   220
          //{{{
27955
4c32c5e75eca use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents: 27949
diff changeset
   221
          val s = output.take
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   222
          if (s == "\u0000") {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   223
            writer.close
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   224
            finished = true
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   225
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   226
          else {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   227
            put_result(Kind.STDIN, s)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   228
            writer.write(s)
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   229
            writer.flush
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   230
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   231
          //}}}
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   232
        }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   233
        catch {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   234
          case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   235
        }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   236
      }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   237
      put_result(Kind.SYSTEM, "Stdin thread terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   238
    }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   239
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   240
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   241
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   242
  /* stdout */
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   243
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   244
  private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   245
    override def run() = {
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31498
diff changeset
   246
      val reader = new BufferedReader(new InputStreamReader(in_stream, Isabelle_System.charset))
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   247
      var result = new StringBuilder(100)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   248
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   249
      var finished = false
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   250
      while (!finished) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   251
        try {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   252
          //{{{
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   253
          var c = -1
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   254
          var done = false
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   255
          while (!done && (result.length == 0 || reader.ready)) {
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   256
            c = reader.read
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   257
            if (c >= 0) result.append(c.asInstanceOf[Char])
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   258
            else done = true
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   259
          }
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   260
          if (result.length > 0) {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   261
            put_result(Kind.STDOUT, result.toString)
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   262
            result.length = 0
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   263
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   264
          else {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   265
            reader.close
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   266
            finished = true
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   267
            try_close()
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   268
          }
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   269
          //}}}
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   270
        }
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   271
        catch {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   272
          case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   273
        }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   274
      }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   275
      put_result(Kind.SYSTEM, "Stdout thread terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   276
    }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   277
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   278
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   279
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   280
  /* messages */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   281
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   282
  private class MessageThread(fifo: String) extends Thread("isabelle: messages")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   283
  {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   284
    private class Protocol_Error(msg: String) extends Exception(msg)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   285
    override def run()
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   286
    {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   287
      val stream = system.fifo_stream(fifo)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   288
      val default_buffer = new Array[Byte](65536)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   289
      var c = -1
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   290
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   291
      def read_chunk(): List[XML.Tree] =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   292
      {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   293
        //{{{
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   294
        // chunk size
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   295
        var n = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   296
        c = stream.read
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   297
        while (48 <= c && c <= 57) {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   298
          n = 10 * n + (c - 48)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   299
          c = stream.read
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   300
        }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   301
        if (c != 10) throw new Protocol_Error("bad message chunk header")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   302
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   303
        // chunk content
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   304
        val buf =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   305
          if (n <= default_buffer.size) default_buffer
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   306
          else new Array[Byte](n)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   307
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   308
        var i = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   309
        var m = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   310
        do {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   311
          m = stream.read(buf, i, n - i)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   312
          i += m
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   313
        } while (m > 0 && n > i)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   314
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   315
        if (i != n) throw new Protocol_Error("bad message chunk content")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   316
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   317
        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   318
        //}}}
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   319
      }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   320
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   321
      do {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   322
        try {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   323
          //{{{
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   324
          c = stream.read
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   325
          var non_sync = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   326
          while (c >= 0 && c != 2) {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   327
            non_sync += 1
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   328
            c = stream.read
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   329
          }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   330
          if (non_sync > 0)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   331
            throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   332
          if (c == 2) {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   333
            val header = read_chunk()
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   334
            val body = read_chunk()
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   335
            header match {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   336
              case List(XML.Elem(name, props, Nil))
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   337
                  if name.size == 1 && Kind.code.isDefinedAt(name(0)) =>
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   338
                put_result(Kind.code(name(0)), props, body)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   339
              case _ => throw new Protocol_Error("bad header: " + header.toString)
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   340
            }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   341
          }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   342
          //}}}
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   343
        }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   344
        catch {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   345
          case e: IOException =>
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   346
            put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   347
          case e: Protocol_Error =>
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   348
            put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage)
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   349
        }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   350
      } while (c != -1)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   351
      stream.close
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   352
      try_close()
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   353
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   354
      put_result(Kind.SYSTEM, "Message thread terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   355
    }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   356
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   357
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   358
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   359
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   360
  /** main **/
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   361
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   362
  {
28497
40e1cc165b05 added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents: 28344
diff changeset
   363
    /* isabelle version */
40e1cc165b05 added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents: 28344
diff changeset
   364
40e1cc165b05 added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents: 28344
diff changeset
   365
    {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   366
      val (msg, rc) = system.isabelle_tool("version")
28497
40e1cc165b05 added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents: 28344
diff changeset
   367
      if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   368
      put_result(Kind.SYSTEM, msg)
28497
40e1cc165b05 added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents: 28344
diff changeset
   369
    }
40e1cc165b05 added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents: 28344
diff changeset
   370
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   371
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
   372
    /* messages */
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   373
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   374
    val message_fifo = system.mk_fifo()
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   375
    def rm_fifo() = system.rm_fifo(message_fifo)
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   376
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   377
    val message_thread = new MessageThread(message_fifo)
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   378
    message_thread.start
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   379
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   380
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   381
    /* exec process */
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   382
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   383
    try {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   384
      val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   385
      proc = system.execute(true, cmdline: _*)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   386
    }
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   387
    catch {
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   388
      case e: IOException =>
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   389
        rm_fifo()
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   390
        error("Failed to execute Isabelle process: " + e.getMessage)
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27992
diff changeset
   391
    }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   392
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   393
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   394
    /* stdin/stdout */
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   395
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   396
    new StdinThread(proc.getOutputStream).start
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   397
    new StdoutThread(proc.getInputStream).start
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   398
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   399
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   400
    /* exit */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   401
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   402
    new Thread("isabelle: exit") {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   403
      override def run() = {
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   404
        val rc = proc.waitFor()
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   405
        Thread.sleep(300)
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   406
        put_result(Kind.SYSTEM, "Exit thread terminated")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   407
        put_result(Kind.EXIT, rc.toString)
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   408
        rm_fifo()
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   409
      }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   410
    }.start
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   411
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   412
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   413
}