--- 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()
--- 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
}