tuned;
authorwenzelm
Mon Sep 20 21:26:58 2010 +0200 (2010-09-20 ago)
changeset 39573a874ca3f5474
parent 39572 bb3469024b6a
child 39574 91b23d141dbf
tuned;
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Sep 20 21:20:06 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Sep 20 21:26:58 2010 +0200
     1.3 @@ -73,6 +73,44 @@
     1.4        actor { loop { react { case res => Console.println(res) } } }, args: _*)
     1.5  
     1.6  
     1.7 +  /* system log */
     1.8 +
     1.9 +  private val system_results = new mutable.ListBuffer[String]
    1.10 +
    1.11 +  private def system_result(text: String)
    1.12 +  {
    1.13 +    synchronized { system_results += text }
    1.14 +    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    1.15 +  }
    1.16 +
    1.17 +  def syslog(): List[String] = synchronized { system_results.toList }
    1.18 +
    1.19 +
    1.20 +  /* results */
    1.21 +
    1.22 +  private val xml_cache = new XML.Cache(131071)
    1.23 +
    1.24 +  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    1.25 +  {
    1.26 +    if (pid.isEmpty && kind == Markup.INIT) {
    1.27 +      rm_fifos()
    1.28 +      props.find(_._1 == Markup.PID).map(_._1) match {
    1.29 +        case None => system_result("Bad Isabelle process initialization: missing pid")
    1.30 +        case p => pid = p
    1.31 +      }
    1.32 +    }
    1.33 +
    1.34 +    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.35 +    xml_cache.cache_tree(msg)((message: XML.Tree) =>
    1.36 +      receiver ! new Result(message.asInstanceOf[XML.Elem]))
    1.37 +  }
    1.38 +
    1.39 +  private def put_result(kind: String, text: String)
    1.40 +  {
    1.41 +    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
    1.42 +  }
    1.43 +
    1.44 +
    1.45    /* input actors */
    1.46  
    1.47    private case class Input_Text(text: String)
    1.48 @@ -153,44 +191,6 @@
    1.49    def join() { process_manager.join() }
    1.50  
    1.51  
    1.52 -  /* system log */
    1.53 -
    1.54 -  private val system_results = new mutable.ListBuffer[String]
    1.55 -
    1.56 -  private def system_result(text: String)
    1.57 -  {
    1.58 -    synchronized { system_results += text }
    1.59 -    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    1.60 -  }
    1.61 -
    1.62 -  def syslog(): List[String] = synchronized { system_results.toList }
    1.63 -
    1.64 -
    1.65 -  /* results */
    1.66 -
    1.67 -  private val xml_cache = new XML.Cache(131071)
    1.68 -
    1.69 -  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    1.70 -  {
    1.71 -    if (pid.isEmpty && kind == Markup.INIT) {
    1.72 -      rm_fifos()
    1.73 -      props.find(_._1 == Markup.PID).map(_._1) match {
    1.74 -        case None => system_result("Bad Isabelle process initialization: missing pid")
    1.75 -        case p => pid = p
    1.76 -      }
    1.77 -    }
    1.78 -
    1.79 -    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.80 -    xml_cache.cache_tree(msg)((message: XML.Tree) =>
    1.81 -      receiver ! new Result(message.asInstanceOf[XML.Elem]))
    1.82 -  }
    1.83 -
    1.84 -  private def put_result(kind: String, text: String)
    1.85 -  {
    1.86 -    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
    1.87 -  }
    1.88 -
    1.89 -
    1.90    /* signals */
    1.91  
    1.92    @volatile private var pid: Option[String] = None