manage persistent syslog via Session, not Isabelle_Process;
authorwenzelm
Thu Sep 23 15:21:04 2010 +0200 (2010-09-23 ago)
changeset 39626a5d0bcfb95a3
parent 39625 fb0c851e4f9d
child 39627 108901b49210
manage persistent syslog via Session, not Isabelle_Process;
tuned;
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/session_dockable.scala
     1.1 --- a/src/Pure/System/isabelle_process.ML	Thu Sep 23 14:39:29 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Sep 23 15:21:04 2010 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4      val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
     1.5      val _ = init_message out_stream;
     1.6      val _ = Keyword.status ();
     1.7 -    val _ = Output.status (Markup.markup Markup.ready "Prover ready");
     1.8 +    val _ = Output.status (Markup.markup Markup.ready "process ready");
     1.9    in loop in_stream end));
    1.10  
    1.11  end;
     2.1 --- a/src/Pure/System/isabelle_process.scala	Thu Sep 23 14:39:29 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Sep 23 15:21:04 2010 +0200
     2.3 @@ -74,21 +74,13 @@
     2.4        actor { loop { react { case res => Console.println(res) } } }, args: _*)
     2.5  
     2.6  
     2.7 -  /* system log */
     2.8 -
     2.9 -  private val system_results = new mutable.ListBuffer[String]
    2.10 +  /* results */
    2.11  
    2.12    private def system_result(text: String)
    2.13    {
    2.14 -    synchronized { system_results += text }
    2.15      receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
    2.16    }
    2.17  
    2.18 -  def syslog(): List[String] = synchronized { system_results.toList }
    2.19 -
    2.20 -
    2.21 -  /* results */
    2.22 -
    2.23    private val xml_cache = new XML.Cache(131071)
    2.24  
    2.25    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
     3.1 --- a/src/Pure/System/session.scala	Thu Sep 23 14:39:29 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Thu Sep 23 15:21:04 2010 +0200
     3.3 @@ -112,6 +112,9 @@
     3.4    @volatile private var syntax = new Outer_Syntax(system.symbols)
     3.5    def current_syntax(): Outer_Syntax = syntax
     3.6  
     3.7 +  @volatile private var reverse_syslog = List[XML.Elem]()
     3.8 +  def syslog(): List[XML.Elem] = reverse_syslog.reverse
     3.9 +
    3.10    private val global_state = new Volatile(Document.State.init)
    3.11    def current_state(): Document.State = global_state.peek()
    3.12  
    3.13 @@ -188,7 +191,8 @@
    3.14            catch { case _: Document.State.Fail => bad_result(result) }
    3.15          case _ =>
    3.16            if (result.is_exit) prover = null  // FIXME ??
    3.17 -          else if (result.is_syslog || result.is_stdout) { }
    3.18 +          else if (result.is_syslog) reverse_syslog ::= result.message
    3.19 +          else if (result.is_stdout) { }
    3.20            else if (result.is_status) {
    3.21              result.body match {
    3.22                case List(Isar_Document.Assign(id, edits)) =>
     4.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 14:39:29 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 15:21:04 2010 +0200
     4.3 @@ -25,7 +25,10 @@
     4.4    private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
     4.5    readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
     4.6  
     4.7 -  private val syslog = new TextArea
     4.8 +  private def session_syslog(): String =
     4.9 +    Isabelle.session.syslog.map(msg => XML.content(msg).mkString).mkString("\n")
    4.10 +
    4.11 +  private val syslog = new TextArea(session_syslog())
    4.12    syslog.editable = false
    4.13  
    4.14    private val tabs = new TabbedPane {
    4.15 @@ -55,7 +58,10 @@
    4.16          case result: Isabelle_Process.Result =>
    4.17            if (result.is_syslog)
    4.18              Swing_Thread.now {
    4.19 -              syslog.append(XML.content(result.message).mkString + "\n")
    4.20 +              val text = session_syslog()
    4.21 +              if (text != syslog.text) {
    4.22 +                syslog.text = text
    4.23 +              }
    4.24              }
    4.25  
    4.26          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)