# HG changeset patch
# User wenzelm
# Date 1285253328 -7200
# Node ID 08eb2730a8a19789ebb3835383c87b6c0017b4f9
# Parent  f6e82967b5cd5d5f599bd258ab1db86d3dc24539
tuned signature;

diff -r f6e82967b5cd -r 08eb2730a8a1 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Sep 23 16:48:12 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 23 16:48:48 2010 +0200
@@ -113,7 +113,7 @@
   def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var reverse_syslog = List[XML.Elem]()
-  def syslog(): List[XML.Elem] = reverse_syslog.reverse
+  def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
 
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state.peek()
diff -r f6e82967b5cd -r 08eb2730a8a1 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 16:48:12 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Thu Sep 23 16:48:48 2010 +0200
@@ -25,10 +25,7 @@
   private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
   readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
 
-  private def session_syslog(): String =
-    Isabelle.session.syslog.map(msg => XML.content(msg).mkString).mkString("\n")
-
-  private val syslog = new TextArea(session_syslog())
+  private val syslog = new TextArea(Isabelle.session.syslog())
   syslog.editable = false
 
   private val tabs = new TabbedPane {
@@ -58,7 +55,7 @@
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {
-              val text = session_syslog()
+              val text = Isabelle.session.syslog()
               if (text != syslog.text) {
                 syslog.text = text
               }