src/Pure/System/isabelle_process.scala
author wenzelm
Thu Jun 25 13:25:35 2009 +0200 (2009-06-25 ago)
changeset 31797 203d5e61e3bc
parent 31498 be0f7f4f9e12
child 32448 a89f876731c5
permissions -rw-r--r--
renamed IsabelleProcess to Isabelle_Process;
renamed IsabelleSystem to Isabelle_System;
     1 /*  Title:      Pure/System/isabelle_process.ML
     2     Author:     Makarius
     3     Options:    :folding=explicit:collapseFolds=1:
     4 
     5 Isabelle process management -- always reactive due to multi-threaded I/O.
     6 */
     7 
     8 package isabelle
     9 
    10 import java.util.concurrent.LinkedBlockingQueue
    11 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
    12   InputStream, OutputStream, IOException}
    13 
    14 
    15 object Isabelle_Process {
    16 
    17   /* results */
    18 
    19   object Kind extends Enumeration {
    20     //{{{ values and codes
    21     // internal system notification
    22     val SYSTEM = Value("SYSTEM")
    23     // Posix channels/events
    24     val STDIN = Value("STDIN")
    25     val STDOUT = Value("STDOUT")
    26     val SIGNAL = Value("SIGNAL")
    27     val EXIT = Value("EXIT")
    28     // Isabelle messages
    29     val INIT = Value("INIT")
    30     val STATUS = Value("STATUS")
    31     val WRITELN = Value("WRITELN")
    32     val PRIORITY = Value("PRIORITY")
    33     val TRACING = Value("TRACING")
    34     val WARNING = Value("WARNING")
    35     val ERROR = Value("ERROR")
    36     val DEBUG = Value("DEBUG")
    37     // messages codes
    38     val code = Map(
    39       ('A' : Int) -> Kind.INIT,
    40       ('B' : Int) -> Kind.STATUS,
    41       ('C' : Int) -> Kind.WRITELN,
    42       ('D' : Int) -> Kind.PRIORITY,
    43       ('E' : Int) -> Kind.TRACING,
    44       ('F' : Int) -> Kind.WARNING,
    45       ('G' : Int) -> Kind.ERROR,
    46       ('H' : Int) -> Kind.DEBUG,
    47       ('0' : Int) -> Kind.SYSTEM,
    48       ('1' : Int) -> Kind.STDIN,
    49       ('2' : Int) -> Kind.STDOUT,
    50       ('3' : Int) -> Kind.SIGNAL,
    51       ('4' : Int) -> Kind.EXIT)
    52     // message markup
    53     val markup = Map(
    54       Kind.INIT -> Markup.INIT,
    55       Kind.STATUS -> Markup.STATUS,
    56       Kind.WRITELN -> Markup.WRITELN,
    57       Kind.PRIORITY -> Markup.PRIORITY,
    58       Kind.TRACING -> Markup.TRACING,
    59       Kind.WARNING -> Markup.WARNING,
    60       Kind.ERROR -> Markup.ERROR,
    61       Kind.DEBUG -> Markup.DEBUG,
    62       Kind.SYSTEM -> Markup.SYSTEM,
    63       Kind.STDIN -> Markup.STDIN,
    64       Kind.STDOUT -> Markup.STDOUT,
    65       Kind.SIGNAL -> Markup.SIGNAL,
    66       Kind.EXIT -> Markup.EXIT)
    67     //}}}
    68     def is_raw(kind: Value) =
    69       kind == STDOUT
    70     def is_control(kind: Value) =
    71       kind == SYSTEM ||
    72       kind == SIGNAL ||
    73       kind == EXIT
    74     def is_system(kind: Value) =
    75       kind == SYSTEM ||
    76       kind == STDIN ||
    77       kind == SIGNAL ||
    78       kind == EXIT ||
    79       kind == STATUS
    80   }
    81 
    82   class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
    83     override def toString = {
    84       val trees = YXML.parse_body_failsafe(result)
    85       val res =
    86         if (kind == Kind.STATUS) trees.map(_.toString).mkString
    87         else trees.flatMap(XML.content(_).mkString).mkString
    88       if (props.isEmpty)
    89         kind.toString + " [[" + res + "]]"
    90       else
    91         kind.toString + " " +
    92           (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    93     }
    94     def is_raw = Kind.is_raw(kind)
    95     def is_control = Kind.is_control(kind)
    96     def is_system = Kind.is_system(kind)
    97   }
    98 
    99   def parse_message(isabelle_system: Isabelle_System, result: Result) =
   100   {
   101     XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
   102       YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
   103   }
   104 }
   105 
   106 
   107 class Isabelle_Process(isabelle_system: Isabelle_System,
   108   results: EventBus[Isabelle_Process.Result], args: String*)
   109 {
   110   import Isabelle_Process._
   111 
   112 
   113   /* demo constructor */
   114 
   115   def this(args: String*) =
   116     this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*)
   117 
   118 
   119   /* process information */
   120 
   121   @volatile private var proc: Process = null
   122   @volatile private var closing = false
   123   @volatile private var pid: String = null
   124   @volatile private var the_session: String = null
   125   def session = the_session
   126 
   127 
   128   /* results */
   129 
   130   def parse_message(result: Result): XML.Tree =
   131     Isabelle_Process.parse_message(isabelle_system, result)
   132 
   133   private val result_queue = new LinkedBlockingQueue[Result]
   134 
   135   private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
   136   {
   137     if (kind == Kind.INIT) {
   138       val map = Map(props: _*)
   139       if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
   140       if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
   141     }
   142     result_queue.put(new Result(kind, props, result))
   143   }
   144 
   145   private class ResultThread extends Thread("isabelle: results") {
   146     override def run() = {
   147       var finished = false
   148       while (!finished) {
   149         val result =
   150           try { result_queue.take }
   151           catch { case _: NullPointerException => null }
   152 
   153         if (result != null) {
   154           results.event(result)
   155           if (result.kind == Kind.EXIT) finished = true
   156         }
   157         else finished = true
   158       }
   159     }
   160   }
   161 
   162 
   163   /* signals */
   164 
   165   def interrupt() = synchronized {
   166     if (proc == null) error("Cannot interrupt Isabelle: no process")
   167     if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
   168     else {
   169       try {
   170         if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
   171           put_result(Kind.SIGNAL, Nil, "INT")
   172         else
   173           put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
   174       }
   175       catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
   176     }
   177   }
   178 
   179   def kill() = synchronized {
   180     if (proc == 0) error("Cannot kill Isabelle: no process")
   181     else {
   182       try_close()
   183       Thread.sleep(500)
   184       put_result(Kind.SIGNAL, Nil, "KILL")
   185       proc.destroy
   186       proc = null
   187       pid = null
   188     }
   189   }
   190 
   191 
   192   /* output being piped into the process */
   193 
   194   private val output = new LinkedBlockingQueue[String]
   195 
   196   private def output_raw(text: String) = synchronized {
   197     if (proc == null) error("Cannot output to Isabelle: no process")
   198     if (closing) error("Cannot output to Isabelle: already closing")
   199     output.put(text)
   200   }
   201 
   202   def output_sync(text: String) =
   203     output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
   204 
   205 
   206   def command(text: String) =
   207     output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
   208 
   209   def command(props: List[(String, String)], text: String) =
   210     output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
   211       IsabelleSyntax.encode_string(text))
   212 
   213   def ML(text: String) =
   214     output_sync("ML_val " + IsabelleSyntax.encode_string(text))
   215 
   216   def close() = synchronized {    // FIXME watchdog/timeout
   217     output_raw("\u0000")
   218     closing = true
   219   }
   220 
   221   def try_close() = synchronized {
   222     if (proc != null && !closing) {
   223       try { close() }
   224       catch { case _: RuntimeException => }
   225     }
   226   }
   227 
   228 
   229   /* stdin */
   230 
   231   private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
   232     override def run() = {
   233       val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Isabelle_System.charset))
   234       var finished = false
   235       while (!finished) {
   236         try {
   237           //{{{
   238           val s = output.take
   239           if (s == "\u0000") {
   240             writer.close
   241             finished = true
   242           }
   243           else {
   244             put_result(Kind.STDIN, Nil, s)
   245             writer.write(s)
   246             writer.flush
   247           }
   248           //}}}
   249         }
   250         catch {
   251           case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
   252         }
   253       }
   254       put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
   255     }
   256   }
   257 
   258 
   259   /* stdout */
   260 
   261   private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
   262     override def run() = {
   263       val reader = new BufferedReader(new InputStreamReader(in_stream, Isabelle_System.charset))
   264       var result = new StringBuilder(100)
   265 
   266       var finished = false
   267       while (!finished) {
   268         try {
   269           //{{{
   270           var c = -1
   271           var done = false
   272           while (!done && (result.length == 0 || reader.ready)) {
   273             c = reader.read
   274             if (c >= 0) result.append(c.asInstanceOf[Char])
   275             else done = true
   276           }
   277           if (result.length > 0) {
   278             put_result(Kind.STDOUT, Nil, result.toString)
   279             result.length = 0
   280           }
   281           else {
   282             reader.close
   283             finished = true
   284             try_close()
   285           }
   286           //}}}
   287         }
   288         catch {
   289           case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
   290         }
   291       }
   292       put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
   293     }
   294   }
   295 
   296 
   297   /* messages */
   298 
   299   private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
   300     override def run() = {
   301       val reader = isabelle_system.fifo_reader(fifo)
   302       var kind: Kind.Value = null
   303       var props: List[(String, String)] = Nil
   304       var result = new StringBuilder
   305 
   306       var finished = false
   307       while (!finished) {
   308         try {
   309           if (kind == null) {
   310             //{{{ Char mode -- resync
   311             var c = -1
   312             do {
   313               c = reader.read
   314               if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
   315             } while (c >= 0 && c != 2)
   316 
   317             if (result.length > 0) {
   318               put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
   319               result.length = 0
   320             }
   321             if (c < 0) {
   322               reader.close
   323               finished = true
   324               try_close()
   325             }
   326             else {
   327               c = reader.read
   328               if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
   329               else kind = null
   330             }
   331             //}}}
   332           }
   333           else {
   334             //{{{ Line mode
   335             val line = reader.readLine
   336             if (line == null) {
   337               reader.close
   338               finished = true
   339               try_close()
   340             }
   341             else {
   342               val len = line.length
   343               // property
   344               if (line.endsWith("\u0002,")) {
   345                 val i = line.indexOf('=')
   346                 if (i > 0) {
   347                   val name = line.substring(0, i)
   348                   val value = line.substring(i + 1, len - 2)
   349                   props = (name, value) :: props
   350                 }
   351               }
   352               // last text line
   353               else if (line.endsWith("\u0002.")) {
   354                 result.append(line.substring(0, len - 2))
   355                 put_result(kind, props.reverse, result.toString)
   356                 kind = null
   357                 props = Nil
   358                 result.length = 0
   359               }
   360               // text line
   361               else {
   362                 result.append(line)
   363                 result.append('\n')
   364               }
   365             }
   366             //}}}
   367           }
   368         }
   369         catch {
   370           case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
   371         }
   372       }
   373       put_result(Kind.SYSTEM, Nil, "Message thread terminated")
   374     }
   375   }
   376 
   377 
   378 
   379   /** main **/
   380 
   381   {
   382     /* isabelle version */
   383 
   384     {
   385       val (msg, rc) = isabelle_system.isabelle_tool("version")
   386       if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
   387       put_result(Kind.SYSTEM, Nil, msg)
   388     }
   389 
   390 
   391     /* messages */
   392 
   393     val message_fifo = isabelle_system.mk_fifo()
   394     def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
   395 
   396     val message_thread = new MessageThread(message_fifo)
   397     message_thread.start
   398 
   399     new ResultThread().start
   400 
   401 
   402     /* exec process */
   403 
   404     try {
   405       val cmdline =
   406         List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
   407       proc = isabelle_system.execute(true, cmdline: _*)
   408     }
   409     catch {
   410       case e: IOException =>
   411         rm_fifo()
   412         error("Failed to execute Isabelle process: " + e.getMessage)
   413     }
   414 
   415 
   416     /* stdin/stdout */
   417 
   418     new StdinThread(proc.getOutputStream).start
   419     new StdoutThread(proc.getInputStream).start
   420 
   421 
   422     /* exit */
   423 
   424     new Thread("isabelle: exit") {
   425       override def run() = {
   426         val rc = proc.waitFor()
   427         Thread.sleep(300)
   428         put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
   429         put_result(Kind.EXIT, Nil, Integer.toString(rc))
   430         rm_fifo()
   431       }
   432     }.start
   433 
   434   }
   435 }