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