tuned;

--- a/src/Tools/jEdit/src/info_dockable.scala	Mon Oct 27 15:16:32 2025 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Mon Oct 27 15:24:25 2025 +0100
@@ -16,34 +16,21 @@
 
 
 object Info_Dockable {
-  /* implicit arguments -- owned by GUI thread */
+  /* content as implicit parameter -- owned by GUI thread */
 
-  private var implicit_snapshot = Document.Snapshot.init
-  private var implicit_results = Command.Results.empty
-  private var implicit_info: List[XML.Elem] = Nil
+  private var _content = Editor.Output.init
 
-  private def set_implicit(
-    snapshot: Document.Snapshot,
-    results: Command.Results,
-    info: List[XML.Elem]
-  ): Unit = {
-    GUI_Thread.require {}
-
-    implicit_snapshot = snapshot
-    implicit_results = results
-    implicit_info = info
-  }
-
-  private def reset_implicit(): Unit =
-    set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
+  private def get_content(): Editor.Output = GUI_Thread.require { _content }
+  private def set_content(content: Editor.Output): Unit = GUI_Thread.require { _content = content }
+  private def reset_content(): Unit = set_content(Editor.Output.init)
 
   def apply(
     view: View,
     snapshot: Document.Snapshot,
     results: Command.Results,
-    info: List[XML.Elem]
+    messages: List[XML.Elem]
   ): Unit = {
-    set_implicit(snapshot, results, info)
+    set_content(Editor.Output(snapshot = snapshot, results = results, messages = messages))
     view.getDockableWindowManager.floatDockableWindow("isabelle-info")
   }
 }
@@ -55,16 +42,12 @@
 
   /* component state -- owned by GUI thread */
 
-  private val snapshot = Info_Dockable.implicit_snapshot
-  private val results = Info_Dockable.implicit_results
-  private val info = Info_Dockable.implicit_info
+  private val content = Info_Dockable.get_content()
 
   private val window_focus_listener =
     new WindowFocusListener {
-      def windowGainedFocus(e: WindowEvent): Unit =
-        Info_Dockable.set_implicit(snapshot, results, info)
-      def windowLostFocus(e: WindowEvent): Unit =
-        Info_Dockable.reset_implicit()
+      def windowGainedFocus(e: WindowEvent): Unit = Info_Dockable.set_content(content)
+      def windowLostFocus(e: WindowEvent): Unit = Info_Dockable.reset_content()
     }
 
 
@@ -75,7 +58,7 @@
       override def handle_shown(): Unit = split_pane_layout()
     }
 
-  output.pretty_text_area.update(snapshot, results, info)
+  output.pretty_text_area.update_output(content)
 
   private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI