# HG changeset patch
# User wenzelm
# Date 1285248064 -7200
# Node ID a5d0bcfb95a329cf3d856f5c2899cd62bc31da7d
# Parent  fb0c851e4f9d9c64c6e25a2e427cc20bcd64d126
manage persistent syslog via Session, not Isabelle_Process;
tuned;

diff -r fb0c851e4f9d -r a5d0bcfb95a3 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Sep 23 14:39:29 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Sep 23 15:21:04 2010 +0200
@@ -182,7 +182,7 @@
     val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
     val _ = init_message out_stream;
     val _ = Keyword.status ();
-    val _ = Output.status (Markup.markup Markup.ready "Prover ready");
+    val _ = Output.status (Markup.markup Markup.ready "process ready");
   in loop in_stream end));
 
 end;
diff -r fb0c851e4f9d -r a5d0bcfb95a3 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Sep 23 14:39:29 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Sep 23 15:21:04 2010 +0200
@@ -74,21 +74,13 @@
       actor { loop { react { case res => Console.println(res) } } }, args: _*)
 
 
-  /* system log */
-
-  private val system_results = new mutable.ListBuffer[String]
+  /* results */
 
   private def system_result(text: String)
   {
-    synchronized { system_results += text }
     receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
   }
 
-  def syslog(): List[String] = synchronized { system_results.toList }
-
-
-  /* results */
-
   private val xml_cache = new XML.Cache(131071)
 
   private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
diff -r fb0c851e4f9d -r a5d0bcfb95a3 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Sep 23 14:39:29 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 23 15:21:04 2010 +0200
@@ -112,6 +112,9 @@
   @volatile private var syntax = new Outer_Syntax(system.symbols)
   def current_syntax(): Outer_Syntax = syntax
 
+  @volatile private var reverse_syslog = List[XML.Elem]()
+  def syslog(): List[XML.Elem] = reverse_syslog.reverse
+
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state.peek()
 
@@ -188,7 +191,8 @@
           catch { case _: Document.State.Fail => bad_result(result) }
         case _ =>
           if (result.is_exit) prover = null  // FIXME ??
-          else if (result.is_syslog || result.is_stdout) { }
+          else if (result.is_syslog) reverse_syslog ::= result.message
+          else if (result.is_stdout) { }
           else if (result.is_status) {
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>
diff -r fb0c851e4f9d -r a5d0bcfb95a3 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 14:39:29 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 15:21:04 2010 +0200
@@ -25,7 +25,10 @@
   private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
   readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
 
-  private val syslog = new TextArea
+  private def session_syslog(): String =
+    Isabelle.session.syslog.map(msg => XML.content(msg).mkString).mkString("\n")
+
+  private val syslog = new TextArea(session_syslog())
   syslog.editable = false
 
   private val tabs = new TabbedPane {
@@ -55,7 +58,10 @@
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {
-              syslog.append(XML.content(result.message).mkString + "\n")
+              val text = session_syslog()
+              if (text != syslog.text) {
+                syslog.text = text
+              }
             }
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)