# HG changeset patch
# User wenzelm
# Date 1667993540 -3600
# Node ID 1eed7e1300ed8ba706e7c7d4afe12c50af920f36
# Parent  304ae1a6e160ce3c03452466e82b88ba95012b4b
clarified signature: more public operations;

diff -r 304ae1a6e160 -r 1eed7e1300ed src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Nov 09 12:05:32 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Nov 09 12:32:20 2022 +0100
@@ -85,20 +85,22 @@
 
   /* syslog */
 
-  private[Session] class Syslog(limit: Int) {
-    private var queue = Queue.empty[XML.Elem]
+  class Syslog(limit: Int) {
+    private var queue = Queue.empty[String]
     private var length = 0
 
-    def += (msg: XML.Elem): Unit = synchronized {
+    def += (msg: String): Unit = synchronized {
       queue = queue.enqueue(msg)
       length += 1
       if (length > limit) queue = queue.dequeue._2
     }
 
-    def content: String = synchronized {
-      cat_lines(queue.iterator.map(XML.content)) +
+    def content(): String = synchronized {
+      cat_lines(queue.iterator) +
       (if (length > limit) "\n(A total of " + length + " messages...)" else "")
     }
+
+    override def toString: String = "Syslog(" + length + ")"
   }
 
 
@@ -221,8 +223,9 @@
 
   /* syslog */
 
-  private val syslog = new Session.Syslog(syslog_limit)
-  def syslog_content(): String = syslog.content
+  def make_syslog(): Session.Syslog = new Session.Syslog(syslog_limit)
+
+  val syslog: Session.Syslog = make_syslog()
 
 
   /* pipelined change parsing */
@@ -577,7 +580,7 @@
         arg match {
           case output: Prover.Output =>
             if (output.is_syslog) {
-              syslog += output.message
+              syslog += XML.content(output.message)
               syslog_messages.post(output)
             }
 
diff -r 304ae1a6e160 -r 1eed7e1300ed src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Nov 09 12:05:32 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala	Wed Nov 09 12:32:20 2022 +0100
@@ -56,7 +56,7 @@
         startup.fulfill("")
       case Session.Terminated(result) =>
         if (!result.ok && !startup.is_finished) {
-          val syslog = session.syslog_content()
+          val syslog = session.syslog.content()
           val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
           startup.fulfill(err)
         }
diff -r 304ae1a6e160 -r 1eed7e1300ed src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Wed Nov 09 12:05:32 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Wed Nov 09 12:32:20 2022 +0100
@@ -183,7 +183,7 @@
     case Session.Terminated(result) if !result.ok =>
       GUI_Thread.later {
         GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
-          "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
+          "Isabelle Syslog", GUI.scrollable_text(session.syslog.content()))
       }
 
     case Session.Ready if !shutting_down.value =>
diff -r 304ae1a6e160 -r 1eed7e1300ed src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Wed Nov 09 12:05:32 2022 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Wed Nov 09 12:32:20 2022 +0100
@@ -20,7 +20,7 @@
   private val syslog = new TextArea()
 
   private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
-    val text = PIDE.session.syslog_content()
+    val text = PIDE.session.syslog.content()
     if (text != syslog.text) syslog.text = text
   }