# HG changeset patch
# User desharna
# Date 1668064408 -3600
# Node ID 1cebb0ca6d86902dd570b17e6836c1c329263ef9
# Parent  0fbfb4293ff714a997a00fded262f0af20d0045c# Parent  9686049ce9889da6bf43dbc0ac65bf621d8fdcfb
merged

diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -9,11 +9,14 @@
 import java.util.{Map => JMap}
 import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
   Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
+import java.awt.event.{KeyAdapter, KeyEvent, ItemListener, ItemEvent}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
-  JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea}
+  JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
+
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
+  Orientation}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 
@@ -127,9 +130,74 @@
     reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
   }
 
-  class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
+
+  /* list selector */
+
+  object Selector {
+    sealed abstract class Entry[A] {
+      def get_item: Option[A] =
+        this match {
+          case item: Item[_] => Some(item.item)
+          case _ => None
+        }
+    }
+    case class Item[A](item: A, description: String = "", batch: Int = 0) extends Entry[A] {
+      override def toString: String = proper_string(description) getOrElse item.toString
+    }
+    case class Separator[A](name: String = "", batch: Int = 0) extends Entry[A] {
+      override def toString: String = "<b>" + name + "</b>"
+    }
+
+    def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch)
+    def separator(batch: Int = 0): Separator[String] = Separator(batch = batch)
+  }
+
+  class Selector[A](val entries: List[Selector.Entry[A]])
+  extends ComboBox[Selector.Entry[A]](entries) {
     def changed(): Unit = {}
 
+    override lazy val peer: JComboBox[Selector.Entry[A]] =
+      new JComboBox[Selector.Entry[A]](ComboBox.newConstantModel(entries)) with SuperMixin {
+        private var key_released = false
+        private var sep_selected = false
+
+        addKeyListener(new KeyAdapter {
+          override def keyPressed(e: KeyEvent): Unit = { key_released = false }
+          override def keyReleased(e: KeyEvent): Unit = { key_released = true }
+        })
+
+        override def setSelectedIndex(i: Int): Unit = {
+          getItemAt(i) match {
+            case _: Selector.Separator[_] =>
+              if (key_released) { sep_selected = true }
+              else {
+                val k = getSelectedIndex()
+                val j = if (i > k) i + 1 else i - 1
+                if (0 <= j && j < dataModel.getSize()) super.setSelectedIndex(j)
+              }
+            case _ => super.setSelectedIndex(i)
+          }
+        }
+
+        override def setPopupVisible(visible: Boolean): Unit = {
+          if (sep_selected) { sep_selected = false}
+          else super.setPopupVisible(visible)
+        }
+      }
+
+    private val default_renderer = renderer
+    private val render_separator = new Separator
+    private val render_label = new Label
+    renderer =
+      (list: ListView[_ <: Selector.Entry[A]], selected: Boolean, focus: Boolean, entry: Selector.Entry[A], i: Int) => {
+        entry match {
+          case sep: Selector.Separator[_] =>
+            if (sep.name.isEmpty) render_separator
+            else { render_label.text = entry.toString; render_label }
+          case _ => default_renderer.componentFor(list, selected, focus, entry, i)
+        }
+      }
+
     listenTo(selection)
     reactions += { case SelectionChanged(_) => changed() }
   }
@@ -141,8 +209,9 @@
 
   class Zoom extends Selector[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
+      .map(GUI.Selector.item(_))
   ) {
-    def factor: Int = parse(selection.item)
+    def factor: Int = parse(selection.item.toString)
 
     private def parse(text: String): Int =
       text match {
@@ -161,7 +230,8 @@
       }
     }
 
-    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
+    makeEditable()(c =>
+      new ComboBox.BuiltInEditor(c)(text => Selector.Item(print(parse(text))), _.toString))
     peer.getEditor.getEditorComponent match {
       case text: JTextField => text.setColumns(4)
       case _ =>
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Nov 10 08:13:28 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 0fbfb4293ff7 -r 1cebb0ca6d86 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala	Thu Nov 10 08:13:28 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 0fbfb4293ff7 -r 1cebb0ca6d86 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -507,6 +507,9 @@
 
     def dirs: List[Path] = dir :: directories
 
+    def main_group: Boolean = groups.contains("main")
+    def doc_group: Boolean = groups.contains("doc")
+
     def timeout_ignored: Boolean =
       !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
 
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -85,12 +85,14 @@
     }
   }
 
-  def dictionaries: List[Dictionary] =
+  lazy val dictionaries: List[Dictionary] =
     for {
       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
       if path.is_file
     } yield new Dictionary(path)
 
+  def get_dictionary(lang: String): Option[Dictionary] = dictionaries.find(_.lang == lang)
+
 
   /* create spell checker */
 
@@ -260,7 +262,7 @@
     if (options.bool("spell_checker")) {
       val lang = options.string("spell_checker_dictionary")
       if (current_spell_checker._1 != lang) {
-        Spell_Checker.dictionaries.find(_.lang == lang) match {
+        Spell_Checker.get_dictionary(lang) match {
           case Some(dictionary) =>
             val spell_checker =
               Exn.capture { Spell_Checker(dictionary) } match {
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -18,8 +18,40 @@
 
 
 object Document_Dockable {
-  def document_output(): Path =
-    Path.explode("$ISABELLE_HOME_USER/document/root.pdf")
+  /* document output */
+
+  def document_name: String = "document"
+  def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
+  def document_output(): Path = document_output_dir() + Path.basic(document_name)
+
+  def view_document(): Unit = {
+    val path = Document_Dockable.document_output().pdf
+    if (path.is_file) Isabelle_System.pdf_viewer(path)
+  }
+
+  class Log_Progress extends Progress {
+    def show(text: String): Unit = {}
+
+    private val syslog = PIDE.session.make_syslog()
+
+    private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) }
+    private val delay =
+      Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() }
+
+    override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
+    override def theory(theory: Progress.Theory): Unit = echo(theory.message)
+
+    def load(): Unit = {
+      val path = document_output().log
+      val text = if (path.is_file) File.read(path) else ""
+      GUI_Thread.later { delay.revoke(); update(text) }
+    }
+
+    update()
+  }
+
+
+  /* state */
 
   object Status extends Enumeration {
     val WAITING = Value("waiting")
@@ -32,16 +64,15 @@
   }
 
   object State {
-    val empty: State = State()
+    def empty(): State = State()
     def finish(result: Result): State = State(output = result.output)
   }
 
   sealed case class State(
-    progress: Progress = new Progress,
+    progress: Log_Progress = new Log_Progress,
     process: Future[Unit] = Future.value(()),
     output: List[XML.Tree] = Nil,
-    status: Status.Value = Status.FINISHED
-  )
+    status: Status.Value = Status.FINISHED)
 }
 
 class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
@@ -50,7 +81,7 @@
 
   /* component state -- owned by GUI thread */
 
-  private val current_state = Synchronized(Document_Dockable.State.empty)
+  private val current_state = Synchronized(Document_Dockable.State.empty())
 
   private val process_indicator = new Process_Indicator
   private val pretty_text_area = new Pretty_Text_Area(view)
@@ -94,28 +125,22 @@
 
   /* progress log */
 
-  private val log_area = new TextArea {
-    editable = false
-    columns = 60
-    rows = 24
-  }
-  log_area.font = GUI.copy_font((new Label).font)
-
+  private val log_area =
+    new TextArea {
+      editable = false
+      font = GUI.copy_font((new Label).font)
+    }
   private val scroll_log_area = new ScrollPane(log_area)
 
-  private def init_progress() = {
-    GUI_Thread.later { log_area.text = "" }
-    new Progress {
-      override def echo(txt: String): Unit =
-        GUI_Thread.later {
-          log_area.append(txt + "\n")
+  def init_progress(): Document_Dockable.Log_Progress =
+    new Document_Dockable.Log_Progress {
+      override def show(text: String): Unit =
+        if (text != log_area.text) {
+          log_area.text = text
           val vertical = scroll_log_area.peer.getVerticalScrollBar
           vertical.setValue(vertical.getMaximum)
         }
-
-      override def theory(theory: Progress.Theory): Unit = echo(theory.message)
     }
-  }
 
 
   /* document build process */
@@ -123,6 +148,9 @@
   private def cancel(): Unit =
     current_state.change { st => st.process.cancel(); st }
 
+  private def init_state(): Unit =
+    current_state.change { _ => Document_Dockable.State(progress = init_progress()) }
+
   private def build_document(): Unit = {
     current_state.change { st =>
       if (st.process.is_finished) {
@@ -133,7 +161,10 @@
             val res =
               Exn.capture {
                 progress.echo("Start " + Date.now())
-                Time.seconds(2.0).sleep()
+                for (i <- 1 to 200) {
+                  progress.echo("message " + i)
+                  Time.seconds(0.1).sleep()
+                }
                 progress.echo("Stop " + Date.now())
               }
             val msg =
@@ -153,18 +184,20 @@
     show_state()
   }
 
-  private def view_document(): Unit = {
-    val path = Document_Dockable.document_output()
-    if (path.is_file) Isabelle_System.pdf_viewer(path)
-  }
-
 
   /* controls */
 
-  private val document_session: GUI.Selector[String] =
-    new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
+  private val document_session: GUI.Selector[String] = {
+    val sessions = JEdit_Sessions.sessions_structure()
+    val all_sessions = sessions.build_topological_order.sorted
+    val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
+    new GUI.Selector(
+      doc_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+      all_sessions.map(GUI.Selector.item(_, batch = 1))
+    ) {
       val title = "Session"
     }
+  }
 
   private val build_button =
     new GUI.Button("<html><b>Build</b></html>") {
@@ -181,7 +214,7 @@
   private val view_button =
     new GUI.Button("View") {
       tooltip = "View document"
-      override def clicked(): Unit = view_document()
+      override def clicked(): Unit = Document_Dockable.view_document()
     }
 
   private val controls =
@@ -204,9 +237,19 @@
       layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
     }, "Output from build process")
 
+  private val load_button =
+    new GUI.Button("Load") {
+      tooltip = "Load final log file"
+      override def clicked(): Unit = current_state.value.progress.load()
+    }
+
+  private val log_controls =
+    Wrap_Panel(List(load_button))
+
   private val log_page =
     new TabbedPane.Page("Log", new BorderPanel {
-      layout(log_area) = BorderPanel.Position.Center
+      layout(log_controls) = BorderPanel.Position.North
+      layout(scroll_log_area) = BorderPanel.Position.Center
     }, "Raw log of build process")
 
   message_pane.pages ++= List(log_page, output_page)
@@ -223,6 +266,7 @@
     }
 
   override def init(): Unit = {
+    init_state()
     PIDE.session.global_options += main
     handle_resize()
   }
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -69,35 +69,38 @@
 
   /* logic selector */
 
-  private sealed case class Logic_Entry(name: String = "", description: String = "") {
-    override def toString: String = proper_string(description) getOrElse name
-  }
-
   def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
-    val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")")
+    val default_entry =
+      GUI.Selector.Item("", description = "default (" + logic_name(options.value) + ")")
 
     val session_entries = {
       val sessions = sessions_structure(options = options.value)
-      val (main_sessions, other_sessions) =
-        sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main"))
-      (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name))
+      val all_sessions = sessions.imports_topological_order
+      val main_sessions = all_sessions.filter(name => sessions(name).main_group)
+
+      main_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+      all_sessions.sorted.map(GUI.Selector.item(_, batch = 1))
     }
 
-    new GUI.Selector[Logic_Entry](default_entry :: session_entries)
-    with JEdit_Options.Entry {
+    new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry {
       name = jedit_logic_option
       tooltip = "Logic session name (change requires restart)"
       val title = "Logic"
       def load(): Unit = {
         val logic = options.string(jedit_logic_option)
-        entries.find(_.name == logic) match {
+        entries.find {
+          case item: GUI.Selector.Item[_] => item.item == logic
+          case _ => false
+        } match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
-      def save(): Unit = options.string(jedit_logic_option) = selection.item.name
+      def save(): Unit =
+        for (item <- selection.item.get_item) options.string(jedit_logic_option) = item
+
       override def changed(): Unit = if (autosave) save()
 
       load()
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -85,18 +85,19 @@
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
-    new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with JEdit_Options.Entry {
+    new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.Item(_))) with JEdit_Options.Entry {
       name = option_name
       tooltip = GUI.tooltip_lines(opt.print_default)
       val title = opt.title()
       def load(): Unit = {
         val lang = PIDE.options.string(option_name)
-        entries.find(_.lang == lang) match {
-          case Some(entry) => selection.item = entry
+        Spell_Checker.get_dictionary(lang) match {
+          case Some(dict) => selection.item = GUI.Selector.Item(dict)
           case None =>
         }
       }
-      def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
+      def save(): Unit =
+        for (item <- selection.item.get_item) PIDE.options.string(option_name) = item.lang
 
       load()
     }
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Thu Nov 10 08:13:28 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 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -64,10 +64,11 @@
 
   /* controls */
 
-  private val select_data = new GUI.Selector[String](ML_Statistics.all_fields.map(_._1)) {
-    tooltip = "Select visualized data collection"
-    override def changed(): Unit = { data_name = selection.item; update_chart() }
-  }
+  private val select_data =
+    new GUI.Selector(ML_Statistics.all_fields.map { case (a, _) => GUI.Selector.item(a) }) {
+      tooltip = "Select visualized data collection"
+      override def changed(): Unit = { data_name = selection.item.toString; update_chart() }
+    }
 
   private val limit_data = new TextField("200", 5) {
     tooltip = "Limit for accumulated data"
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Nov 10 08:13:28 2022 +0100
@@ -60,12 +60,12 @@
                 case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
                 case None => (stack, Nil)
               }
-            old.foreach(_.hide_popup)
+            old.foreach(_.hide_popup())
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
             val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
             stack = tip :: rest
-            tip.show_popup
+            tip.show_popup()
         }
     }
   }
@@ -123,7 +123,7 @@
       case (Nil, _) =>
       case (unfocused, rest) =>
         deactivate()
-        unfocused.foreach(_.hide_popup)
+        unfocused.foreach(_.hide_popup())
         stack = rest
     }
   }
@@ -133,11 +133,11 @@
     hierarchy(tip) match {
       case Some((old, _ :: rest)) =>
         rest match {
-          case top :: _ => top.request_focus
+          case top :: _ => top.request_focus()
           case Nil => JEdit_Lib.request_focus_view()
         }
-        old.foreach(_.hide_popup)
-        tip.hide_popup
+        old.foreach(_.hide_popup())
+        tip.hide_popup()
         stack = rest
       case _ =>
     }
@@ -151,7 +151,7 @@
     if (stack.isEmpty) false
     else {
       JEdit_Lib.request_focus_view()
-      stack.foreach(_.hide_popup)
+      stack.foreach(_.hide_popup())
       stack = Nil
       true
     }
@@ -202,7 +202,7 @@
 
   val pretty_text_area: Pretty_Text_Area =
     new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
-      override def get_background() = Some(rendering.tooltip_color)
+      override def get_background(): Option[Color] = Some(rendering.tooltip_color)
     }
 
   pretty_text_area.addFocusListener(new FocusAdapter {
@@ -269,14 +269,14 @@
     new Popup(layered, tip, screen.relative(layered, size), size)
   }
 
-  private def show_popup: Unit = {
+  private def show_popup(): Unit = {
     popup.show
     pretty_text_area.requestFocus()
     pretty_text_area.update(rendering.snapshot, results, info.info)
   }
 
-  private def hide_popup: Unit = popup.hide
+  private def hide_popup(): Unit = popup.hide
 
-  private def request_focus: Unit = pretty_text_area.requestFocus()
+  private def request_focus(): Unit = pretty_text_area.requestFocus()
 }
 
diff -r 0fbfb4293ff7 -r 1cebb0ca6d86 src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Thu Nov 10 08:13:28 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
   }