merged
authornipkow
Wed, 27 Nov 2024 16:52:04 +0100
changeset 81501 25978a474603
parent 81499 60696404b40a (diff)
parent 81500 d4d34f552eec (current diff)
child 81502 ed766dfdd2f1
child 81503 60e61a934a80
merged
--- a/Admin/build/TUM.toml	Wed Nov 27 16:51:50 2024 +0100
+++ b/Admin/build/TUM.toml	Wed Nov 27 16:52:04 2024 +0100
@@ -1,11 +1,11 @@
 # Build cluster resources at TUM
 
 [host.lxbroy10]
-hostname = "lxbroy10.informatik.tu-muenchen.de"
+hostname = "lxbroy10.in.tum.de"
 numa = true
 
 [host.vmnipkow9]
-hostname = "vmnipkow9.informatik.tu-muenchen.de"
+hostname = "vmnipkow9.in.tum.de"
 
 [host.mini1]
 hostname = "131.159.47.71"
--- a/Admin/etc/options	Wed Nov 27 16:51:50 2024 +0100
+++ b/Admin/etc/options	Wed Nov 27 16:52:04 2024 +0100
@@ -2,7 +2,7 @@
 
 section "Admin tools"
 
-option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de"
+option isabelle_components_server : string = "lxbroy10.in.tum.de"
   -- "user@host for SSH connection"
 
 option isabelle_components_dir : string = "/p/home/isabelle/components"
--- a/NEWS	Wed Nov 27 16:51:50 2024 +0100
+++ b/NEWS	Wed Nov 27 16:52:04 2024 +0100
@@ -139,6 +139,8 @@
   - Highlighting works via mouse hovering alone, without requiring
     C-modifier.
 
+  - Search results are shown as tree view.
+
 * An active highlight area in the input buffer or output panel may be
 turned into a text selection by using the ALT modifier.
 
--- a/src/HOL/Analysis/Cartesian_Space.thy	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Wed Nov 27 16:52:04 2024 +0100
@@ -353,11 +353,6 @@
   shows "invertible (transpose A)"
   by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
 
-lemma vector_matrix_mul_assoc:
-  fixes v :: "('a::comm_semiring_1)^'n"
-  shows "(v v* M) v* N = v v* (M ** N)"
-  by (metis (no_types, opaque_lifting) matrix_transpose_mul matrix_vector_mul_assoc transpose_matrix_vector)
-
 lemma matrix_scaleR_vector_ac:
   fixes A :: "real^('m::finite)^'n"
   shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Nov 27 16:52:04 2024 +0100
@@ -986,7 +986,7 @@
 
 definition\<^marker>\<open>tag important\<close> vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
     (infixl \<open>v*\<close> 70)
-  where "v v* m == (\<chi> j. sum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
+  where "v v* m == (\<chi> j. sum (\<lambda>i. ((v$i) * (m$i)$j)) (UNIV :: 'm set)) :: 'a^'n"
 
 definition\<^marker>\<open>tag unimportant\<close> "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
 definition\<^marker>\<open>tag unimportant\<close> transpose where
@@ -1018,25 +1018,26 @@
   unfolding matrix_matrix_mult_def mat_def
   by (auto simp: if_distrib if_distribR sum.delta'[OF finite] cong: if_cong)
 
-proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
+lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
   apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
-  apply (subst sum.swap)
-  apply simp
-  done
+  using sum.swap by fastforce
 
-proposition matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
+lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
   apply (vector matrix_matrix_mult_def matrix_vector_mult_def
     sum_distrib_left sum_distrib_right mult.assoc)
-  apply (subst sum.swap)
-  apply simp
-  done
+  using sum.swap by fastforce
 
-proposition scalar_matrix_assoc:
+lemma vector_matrix_mul_assoc: "(x v* A) v* B = x v* (A**B)"
+  apply (vector matrix_matrix_mult_def vector_matrix_mult_def
+    sum_distrib_left sum_distrib_right mult.assoc)
+  using sum.swap by fastforce
+
+lemma scalar_matrix_assoc:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)
 
-proposition matrix_scalar_ac:
+lemma matrix_scalar_ac:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
   by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
@@ -1046,6 +1047,13 @@
   apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
   done
 
+lemma vector_matrix_mul_rid [simp]:
+  fixes v :: "('a::semiring_1)^'n"
+  shows "v v* mat 1 = v"
+  apply (vector vector_matrix_mult_def mat_def)
+  apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
+  done
+
 lemma matrix_transpose_mul:
     "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
   by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
@@ -1139,6 +1147,11 @@
   unfolding vector_matrix_mult_def
   by (simp add: algebra_simps sum.distrib vec_eq_iff)
 
+lemma vector_matrix_mult_diff_distrib [algebra_simps]:
+  fixes A :: "'a::ring_1^'n^'m"
+  shows "(x - y) v* A = x v* A - y v* A"
+  by (vector vector_matrix_mult_def sum_subtractf left_diff_distrib)
+
 lemma matrix_vector_right_distrib [algebra_simps]:
   "A *v (x + y) = A *v x + A *v y"
   by (vector matrix_vector_mult_def sum.distrib distrib_left)
@@ -1168,6 +1181,15 @@
   shows "(A - B) *v x = (A *v x) - (B *v x)"
   by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib)
 
+lemma vector_matrix_mult_add_rdistrib [algebra_simps]:
+  "x v* (A + B) = (x v* A) + (x v* B)"
+  by (vector vector_matrix_mult_def sum.distrib distrib_left)
+
+lemma  vector_matrix_mult_diff_rdistrib [algebra_simps]:
+  fixes A :: "'a :: ring_1^'n^'m"
+  shows "x v* (A - B) = (x v* A) - (x v* B)"
+  by (vector vector_matrix_mult_def sum_subtractf right_diff_distrib)
+
 lemma matrix_vector_column:
   "(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
@@ -1201,19 +1223,19 @@
     unfolding invertible_def by auto
 qed
 
-proposition scalar_invertible_iff:
+lemma scalar_invertible_iff:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   assumes "k \<noteq> 0" and "invertible A"
   shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
   by (simp add: assms scalar_invertible)
 
-lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
+lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v (x:: 'a::{comm_semiring_1}^'n)"
   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
-  by simp
+  by (simp add: mult.commute)
 
-lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
+lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* (A:: 'a::{comm_semiring_1}^'m^'n)"
   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
-  by simp
+  by (simp add: mult.commute)
 
 lemma vector_scalar_commute:
   fixes A :: "'a::{field}^'m^'n"
@@ -1231,23 +1253,17 @@
 lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
   unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
 
-lemma vector_matrix_mul_rid [simp]:
-  fixes v :: "('a::semiring_1)^'n"
-  shows "v v* mat 1 = v"
-  by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
-
 lemma scaleR_vector_matrix_assoc:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
   shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
   by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
 
-proposition vector_scaleR_matrix_ac:
+lemma vector_scaleR_matrix_ac:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
   shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
 proof -
   have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
-    unfolding vector_matrix_mult_def
-    by (simp add: algebra_simps)
+    by (simp add: vector_matrix_mult_def algebra_simps)
   with scaleR_vector_matrix_assoc
   show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
     by auto
--- a/src/HOL/Hilbert_Choice.thy	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Wed Nov 27 16:52:04 2024 +0100
@@ -147,6 +147,34 @@
 qed
 
 
+subsection \<open>Getting an element of a nonempty set\<close>
+
+definition some_elem :: "'a set \<Rightarrow> 'a"
+  where "some_elem A = (SOME x. x \<in> A)"
+
+lemma some_elem_eq [simp]: "some_elem {x} = x"
+  by (simp add: some_elem_def)
+
+lemma some_elem_nonempty: "A \<noteq> {} \<Longrightarrow> some_elem A \<in> A"
+  unfolding some_elem_def by (auto intro: someI)
+
+lemma is_singleton_some_elem: "is_singleton A \<longleftrightarrow> A = {some_elem A}"
+  by (auto simp: is_singleton_def)
+
+lemma some_elem_image_unique:
+  assumes "A \<noteq> {}"
+    and *: "\<And>y. y \<in> A \<Longrightarrow> f y = a"
+  shows "some_elem (f ` A) = a"
+  unfolding some_elem_def
+proof (rule some1_equality)
+  from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
+  with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
+  then show "a \<in> f ` A" by auto
+  with * show "\<exists>!x. x \<in> f ` A"
+    by auto
+qed
+
+
 subsection \<open>Function Inverse\<close>
 
 lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
--- a/src/HOL/Set.thy	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/HOL/Set.thy	Wed Nov 27 16:52:04 2024 +0100
@@ -1834,14 +1834,13 @@
 
 lemma the_elem_image_unique:
   assumes "A \<noteq> {}"
-    and *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
-  shows "the_elem (f ` A) = f x"
+    and *: "\<And>y. y \<in> A \<Longrightarrow> f y = a"
+  shows "the_elem (f ` A) = a"
   unfolding the_elem_def
 proof (rule the1_equality)
   from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
-  with * have "f x = f y" by simp
-  with \<open>y \<in> A\<close> have "f x \<in> f ` A" by blast
-  with * show "f ` A = {f x}" by auto
+  with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
+  with * show "f ` A = {a}" by auto
   then show "\<exists>!x. f ` A = {x}" by auto
 qed
 
--- a/src/HOL/Tools/try0.ML	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/HOL/Tools/try0.ML	Wed Nov 27 16:52:04 2024 +0100
@@ -48,8 +48,11 @@
 datatype modifier = Use | Simp | Intro | Elim | Dest
 
 fun string_of_xthm (xref, args) =
-  (case xref of Facts.Fact literal => cartouche literal | _ => Facts.string_of_ref xref) ^
-    implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
+  (case xref of
+    Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
+  | _ =>
+      Facts.string_of_ref xref) ^ implode
+        (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
 
 fun add_attr_text tagged (tag, src) s =
   let
@@ -74,19 +77,16 @@
 
       val ctxt = Proof.context_of st
 
-      val using_text =
-        (K (Method.insert (Attrib.eval_thms ctxt unused)))
-        |> Method.Basic
-
       val text =
         name ^ attrs
         |> parse_method ctxt
         |> Method.method_cmd ctxt
         |> Method.Basic
         |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
-        |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Then, [using_text, m]))
 
-      val apply = text |> Proof.refine #> Seq.filter_results
+      val apply =
+        Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
+        #> Proof.refine text #> Seq.filter_results
       val num_before = num_goals st
       val multiple_goals = all_goals andalso num_before > 1
       val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
--- a/src/Pure/GUI/tree_view.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Pure/GUI/tree_view.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -8,7 +8,7 @@
 
 import javax.swing.JTree
 import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel,
-  TreeSelectionModel}
+  TreeSelectionModel, TreeCellRenderer, DefaultTreeCellRenderer}
 
 
 object Tree_View {
@@ -24,6 +24,24 @@
         case _ => None
       }
   }
+
+  class Cell_Renderer extends DefaultTreeCellRenderer {
+    def setup(value: AnyRef): Unit = setIcon(null)
+
+    override def getTreeCellRendererComponent(
+      tree: JTree,
+      value: AnyRef,
+      selected: Boolean,
+      expanded: Boolean,
+      leaf: Boolean,
+      row: Int,
+      hasFocus: Boolean
+    ): java.awt.Component = {
+      super.getTreeCellRendererComponent(tree, value, selected, expanded, leaf, row, hasFocus)
+      setup(value)
+      this
+    }
+  }
 }
 
 class Tree_View(
@@ -36,9 +54,12 @@
       case _ => None
     }
 
-  def clear(): Unit = {
+  def init_model(body: => Unit): Unit = {
     clearSelection()
     root.removeAllChildren()
+    body
+    expandRow(0)
+    reload_model()
   }
 
   def reload_model(): Unit =
@@ -50,6 +71,8 @@
 
   /* init */
 
+  setCellRenderer(new Tree_View.Cell_Renderer)
+
   setRowHeight(0)
 
   if (single_selection_mode) {
--- a/src/Tools/Graphview/tree_panel.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -12,7 +12,7 @@
 import java.awt.{Dimension, Rectangle}
 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
 import javax.swing.tree.TreePath
-import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
+import javax.swing.event.{DocumentListener, DocumentEvent}
 
 import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, Action}
@@ -140,14 +140,9 @@
 
   def refresh(): Unit = {
     val new_nodes = graphview.visible_graph.topological_order
-    if (new_nodes != nodes) {
-      tree.clear()
-
+    if (nodes != new_nodes) {
       nodes = new_nodes
-      for (node <- nodes) tree.root.add(Tree_View.Node(node))
-
-      tree.expandRow(0)
-      tree.revalidate()
+      tree.init_model { for (node <- nodes) tree.root.add(Tree_View.Node(node)) }
     }
     revalidate()
     repaint()
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -64,10 +64,17 @@
   private var current_output: List[XML.Tree] = Nil
 
 
-  /* pretty text area */
+  /* output area */
 
   private val output: Output_Area =
     new Output_Area(view, root_name = "Threads") {
+      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {}
+
+      override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
+        update_focus()
+        update_vals()
+      }
+
       override def handle_update(): Unit = {
         val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
         val (new_threads, new_output) = debugger.status(tree_selection())
@@ -89,7 +96,8 @@
   override def detach_operation: Option[() => Unit] =
     output.pretty_text_area.detach_operation
 
-  output.init_gui(dockable, split = true)
+  output.setup(dockable)
+  set_content(output.split_pane)
 
 
   /* tree view */
@@ -112,18 +120,16 @@
         case _ => thread_contexts.headOption
       }
 
-    output.tree.clear()
-
-    for (thread <- thread_contexts) {
-      val thread_node = Tree_View.Node(thread)
-      for ((_, i) <- thread.debug_states.zipWithIndex)
-        thread_node.add(Tree_View.Node(thread.select(i)))
-      output.tree.root.add(thread_node)
+    output.tree.init_model {
+      for (thread <- thread_contexts) {
+        val thread_node = Tree_View.Node(thread)
+        for ((_, i) <- thread.debug_states.zipWithIndex) {
+          thread_node.add(Tree_View.Node(thread.select(i)))
+        }
+        output.tree.root.add(thread_node)
+      }
     }
 
-    output.tree.reload_model()
-
-    output.tree.expandRow(0)
     for (i <- Range.inclusive(output.tree.getRowCount - 1, 1, -1)) output.tree.expandRow(i)
 
     new_tree_selection match {
@@ -255,11 +261,6 @@
     JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
   }
 
-  output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) =>
-    update_focus()
-    update_vals()
-  })
-
 
   /* main */
 
@@ -279,14 +280,14 @@
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
     debugger.init(dockable)
-    output.handle_update()
+    output.init()
     jEdit.propertiesChanged()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
-    output.delay_resize.revoke()
+    output.exit()
     debugger.exit(dockable)
     jEdit.propertiesChanged()
   }
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -65,13 +65,16 @@
   private val current_state = Synchronized(Document_Dockable.State.init())
 
   private val process_indicator = new Process_Indicator
-  private val pretty_text_area = new Pretty_Text_Area(view)
+  private val output: Output_Area = new Output_Area(view)
   private val message_pane = new TabbedPane
 
+  override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
+
+
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
-    pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all)
+    output.pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all)
 
     if (st.running) process_indicator.update("Running document build process ...", 15)
     else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5)
@@ -84,21 +87,6 @@
   }
 
 
-  /* text area with zoom/resize */
-
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
-  private val delay_resize: Delay =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-
   /* progress */
 
   class Log_Progress extends Program_Progress(default_title = "build") {
@@ -348,16 +336,18 @@
       override def clicked(): Unit = cancel_process()
     }
 
-  private val output_controls = Wrap_Panel(List(cancel_button, pretty_text_area.zoom_component))
+  private val output_controls =
+    Wrap_Panel(List(cancel_button, output.pretty_text_area.zoom_component))
 
   private val output_page =
     new TabbedPane.Page("Output", new BorderPanel {
       layout(output_controls) = BorderPanel.Position.North
-      layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
+      layout(output.text_pane) = BorderPanel.Position.Center
     }, "Results from document build process")
 
   message_pane.pages ++= List(input_page, output_page)
 
+  output.setup(dockable)
   set_content(message_pane)
 
 
@@ -368,7 +358,7 @@
       case _: Session.Global_Options =>
         GUI_Thread.later {
           document_session.load()
-          handle_resize()
+          output.handle_resize()
           refresh_theories()
         }
       case changed: Session.Commands_Changed =>
@@ -397,14 +387,14 @@
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
-    handle_resize()
+    output.init()
     delay_load.invoke()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
-    delay_resize.revoke()
+    output.exit()
     PIDE.editor.document_exit(dockable)
   }
 }
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -50,6 +50,9 @@
 
 
 class Info_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
+
   /* component state -- owned by GUI thread */
 
   private val snapshot = Info_Dockable.implicit_snapshot
@@ -65,47 +68,34 @@
     }
 
 
-  /* pretty text area */
-
-  private val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  /* output text area */
 
-  pretty_text_area.update(snapshot, results, info)
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
-
-  /* resize */
+  private val output: Output_Area = new Output_Area(view)
+  output.pretty_text_area.update(snapshot, results, info)
 
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
+  private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components)
+  add(controls.peer, BorderLayout.NORTH)
 
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-  private val controls = Wrap_Panel(pretty_text_area.search_zoom_components)
-
-  add(controls.peer, BorderLayout.NORTH)
+  output.setup(dockable)
+  set_content(output.split_pane)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Session.Global_Options](getClass.getName) {
-      case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
+      case _: Session.Global_Options => GUI_Thread.later { output.handle_resize() }
     }
 
   override def init(): Unit = {
     GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main
-    handle_resize()
+    output.init()
   }
 
   override def exit(): Unit = {
     GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main
-    delay_resize.revoke()
+    output.exit()
   }
 }
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -144,6 +144,10 @@
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
+  def can_search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): Boolean =
+    try { regex.findFirstIn(buffer.getSegment(range.start, range.length)).nonEmpty }
+    catch { case _: ArrayIndexOutOfBoundsException => false }
+
   def search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): List[Text.Range] =
     List.from(
       for {
@@ -335,26 +339,23 @@
 
     { (range: Text.Range) =>
       val stop = range.stop
+      try {
+        val p = text_area.offsetToXY(range.start)
+        val (q, r) =
+          if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) {
+            (text_area.offsetToXY(stop - 1), char_width)
+          }
+          else if (stop >= end) {
+            (text_area.offsetToXY(end), char_width * (stop - end))
+          }
+          else (text_area.offsetToXY(stop), 0)
 
-      val (p, q, r) =
-        try {
-          val p = text_area.offsetToXY(range.start)
-          val (q, r) =
-            if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) {
-              (text_area.offsetToXY(stop - 1), char_width)
-            }
-            else if (stop >= end) {
-              (text_area.offsetToXY(end), char_width * (stop - end))
-            }
-            else (text_area.offsetToXY(stop), 0)
-          (p, q, r)
+        if (p != null && q != null && p.x < q.x + r && p.y == q.y) {
+          Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
         }
-        catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
-
-      if (p != null && q != null && p.x < q.x + r && p.y == q.y) {
-        Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
+        else None
       }
-      else None
+      catch { case _: ArrayIndexOutOfBoundsException => None }
     }
   }
 
--- a/src/Tools/jEdit/src/output_area.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -13,26 +13,47 @@
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
 import javax.swing.JComponent
+import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
 
+import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
 import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.View
 
 
-class Output_Area(view: View, root_name: String = "Overview") {
+class Output_Area(view: View, root_name: String = "Search results") {
+  output_area =>
+
   GUI_Thread.require {}
 
 
   /* tree view */
 
+  val tree_cell_renderer: Tree_View.Cell_Renderer = new Tree_View.Cell_Renderer
+
   val tree: Tree_View =
     new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
 
+  def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {
+    tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) }
+    tree.revalidate()
+  }
+
+  def handle_tree_selection(e: TreeSelectionEvent): Unit =
+    for (result <- tree.get_selection({ case x: Pretty_Text_Area.Search_Result => x })) {
+      pretty_text_area.setCaretPosition(result.line_range.start)
+      JEdit_Lib.scroll_to_caret(pretty_text_area)
+    }
+
 
   /* text area */
 
-  val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view)
+  val pretty_text_area: Pretty_Text_Area =
+    new Pretty_Text_Area(view) {
+      override def handle_search(search: Pretty_Text_Area.Search_Results): Unit =
+        output_area.handle_search(search)
+    }
 
   def handle_resize(): Unit = pretty_text_area.zoom()
   def handle_update(): Unit = ()
@@ -69,6 +90,11 @@
       }
     }
 
+  private lazy val tree_selection_listener =
+    new TreeSelectionListener {
+      def valueChanged(e: TreeSelectionEvent): Unit = handle_tree_selection(e)
+    }
+
 
   /* GUI components */
 
@@ -89,13 +115,18 @@
       rightComponent = text_pane
     }
 
-  def init_gui(parent: JComponent, split: Boolean = false): Unit = {
+  def setup(parent: JComponent): Unit = {
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)
     tree.addMouseListener(mouse_listener)
-    parent match {
-      case dockable: Dockable => dockable.set_content(if (split) split_pane else text_pane)
-      case _ =>
-    }
+    tree.addTreeSelectionListener(tree_selection_listener)
+    tree.setCellRenderer(tree_cell_renderer)
   }
+
+  def init(): Unit = {
+    handle_update()
+    handle_resize()
+  }
+
+  def exit(): Unit = delay_resize.revoke()
 }
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -16,23 +16,24 @@
 
 
 class Output_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
+
   /* component state -- owned by GUI thread */
 
   private var do_update = true
   private var current_output: List[XML.Elem] = Nil
 
 
-  /* pretty text area */
+  /* output area */
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  private val output: Output_Area =
+    new Output_Area(view) { override def handle_update(): Unit = dockable.handle_update(true) }
 
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
-
+  override def detach_operation: Option[() => Unit] =
+    output.pretty_text_area.detach_operation
 
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
-  private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
+  private def handle_update(follow: Boolean, restriction: Option[Set[Command]] = None): Unit = {
     GUI_Thread.require {}
 
     for {
@@ -51,12 +52,15 @@
         else current_output
 
       if (current_output != new_output) {
-        pretty_text_area.update(snapshot, results, new_output)
+        output.pretty_text_area.update(snapshot, results, new_output)
         current_output = new_output
       }
     }
   }
 
+  output.setup(dockable)
+  dockable.set_content(output.split_pane)
+
 
   /* controls */
 
@@ -68,19 +72,19 @@
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
       do_update = state
-      handle_update(do_update, None)
+      handle_update(do_update)
     }
   }
 
   private val update_button = new GUI.Button("Update") {
     tooltip = "Update display according to the command at cursor position"
-    override def clicked(): Unit = handle_update(true, None)
+    override def clicked(): Unit = handle_update(true)
   }
 
   private val controls =
     Wrap_Panel(
       List(output_state_button, auto_hovering_button, auto_update_button, update_button) :::
-      pretty_text_area.search_zoom_components)
+      output.pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
@@ -91,42 +95,31 @@
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later {
-          handle_resize()
+          output.handle_resize()
           output_state_button.load()
           auto_hovering_button.load()
-          handle_update(do_update, None)
+          handle_update(do_update)
         }
 
       case changed: Session.Commands_Changed =>
         val restriction = if (changed.assignment) None else Some(changed.commands)
-        GUI_Thread.later { handle_update(do_update, restriction) }
+        GUI_Thread.later { handle_update(do_update, restriction = restriction) }
 
       case Session.Caret_Focus =>
-        GUI_Thread.later { handle_update(do_update, None) }
+        GUI_Thread.later { handle_update(do_update) }
     }
 
   override def init(): Unit = {
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
-    handle_update(true, None)
+    output.init()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     PIDE.session.caret_focus -= main
-    delay_resize.revoke()
+    output.exit()
   }
-
-
-  /* resize */
-
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
 }
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -20,12 +20,85 @@
 import scala.util.matching.Regex
 
 import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
+import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
 import org.gjt.sp.jedit.textarea.JEditEmbeddedTextArea
+import org.gjt.sp.jedit.search.HyperSearchResults
 import org.gjt.sp.jedit.syntax.SyntaxStyle
 import org.gjt.sp.jedit.gui.KeyEventTranslator
-import org.gjt.sp.util.{SyntaxUtilities, Log}
+import org.gjt.sp.util.{SyntaxUtilities, Log, HtmlUtilities}
+
+object Pretty_Text_Area {
+  def make_highlight_style(): String =
+    HtmlUtilities.style2html(jEdit.getProperty(HyperSearchResults.HIGHLIGHT_PROP),
+      Font_Metric.default_font)
+
+  sealed case class Search_Result(
+    buffer: JEditBuffer,
+    highlight_style: String,
+    regex: Regex,
+    line: Int,
+    line_range: Text.Range
+  ) {
+    lazy val line_text: String =
+      Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse(""))
+
+    lazy val gui_text: String = {
+      // see also HyperSearchResults.highlightString
+      val s = new StringBuilder(line_range.length * 2)
+      s ++= "<html><b>"
+      s ++= line.toString
+      s ++= ":</b> "
 
+      val line_start = line_range.start
+      val search_range = Text.Range(line_start, line_start + line_text.length)
+      var last = 0
+      for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) {
+        val next = range.start - line_start
+        if (last < next) s ++= line_text.substring(last, next)
+        s ++= "<span style=\""
+        s ++= highlight_style
+        s ++= "\">"
+        s ++= line_text.substring(next, next + range.length)
+        s ++= "</span>"
+        last = range.stop - line_start
+      }
+      if (last < line_text.length) s ++= line_text.substring(last)
+      s ++= "</html>"
+      s.toString
+    }
+    override def toString: String = gui_text
+  }
+
+  sealed case class Search_Results(
+    buffer: JEditBuffer,
+    highlight_style: String,
+    pattern: Option[Regex] = None,
+    results: List[Search_Result] = Nil
+  ) {
+    val length: Int = results.length
+
+    def update(start_offset: Int): (Int, Search_Results) =
+    pattern match {
+      case None => (length, this)
+      case Some(regex) =>
+        val start_line = buffer.getLineOfOffset(start_offset)
+        val results1 = results.takeWhile(result => result.line < start_line)
+        val results2 =
+          List.from(
+            for {
+              line <- (start_line until buffer.getLineCount).iterator
+              line_range = JEdit_Lib.line_range(buffer, line)
+              if JEdit_Lib.can_search_text(buffer, line_range, regex)
+            } yield Search_Result(buffer, highlight_style, regex, line, line_range))
+        (results1.length, copy(results = results1 ::: results2))
+    }
+
+    def update_pattern(new_pattern: Option[Regex]): Option[Search_Results] =
+      if (pattern == new_pattern) None
+      else Some(copy(pattern = new_pattern, results = Nil).update(0)._2)
+  }
+}
 
 class Pretty_Text_Area(
   view: View,
@@ -55,8 +128,11 @@
     new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action,
       get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
 
-  private var current_search_pattern: Option[Regex] = None
-  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
+  private var current_search_results =
+    Pretty_Text_Area.Search_Results(getBuffer, Pretty_Text_Area.make_highlight_style())
+
+  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_results.pattern }
+  def handle_search(search: Pretty_Text_Area.Search_Results): Unit = ()
 
   def get_background(): Option[Color] = None
 
@@ -130,6 +206,14 @@
                 else if (scroll_start < update_start) scroll_start
                 else 0)
               JEdit_Lib.scroll_to_caret(pretty_text_area)
+
+              val (search_update_start, search_results) =
+                current_search_results.update(update_start)
+              if (current_search_results != search_results) {
+                current_search_results = search_results
+                handle_search(search_results)
+                pretty_text_area.getPainter.repaint()
+              }
             }
           }
         })
@@ -195,13 +279,14 @@
           val re = Library.make_regex(s)
           (re, re.isDefined)
       }
-    if (current_search_pattern != pattern) {
-      current_search_pattern = pattern
-      pretty_text_area.getPainter.repaint()
-    }
     text_field.setForeground(
       if (ok) search_field_foreground
       else current_rendering.color(Rendering.Color.error))
+    for (search_results <- current_search_results.update_pattern(pattern)) {
+      current_search_results = search_results
+      handle_search(search_results)
+      refresh()
+    }
   }
 
 
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -18,6 +18,8 @@
 
 
 class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
@@ -30,8 +32,10 @@
   private var do_update = true
 
 
-  private val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  private val output: Output_Area = new Output_Area(view)
+
+  output.setup(dockable)
+  set_content(output.text_pane)
 
   private def update_contents(): Unit = {
     val snapshot = current_snapshot
@@ -41,8 +45,8 @@
     context.questions.values.toList match {
       case q :: _ =>
         val data = q.data
-        val output = List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0))
-        pretty_text_area.update(snapshot, Command.Results.empty, output)
+        output.pretty_text_area.update(snapshot, Command.Results.empty,
+          List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0)))
         q.answers.foreach { answer =>
           answers.contents += new GUI.Button(answer.string) {
             override def clicked(): Unit =
@@ -50,10 +54,10 @@
           }
         }
       case Nil =>
-        pretty_text_area.update(snapshot, Command.Results.empty, Nil)
+        output.pretty_text_area.update(snapshot, Command.Results.empty, Nil)
     }
 
-    handle_resize()
+    output.handle_resize()
   }
 
   private def show_trace(): Unit = {
@@ -61,8 +65,6 @@
     new Simplifier_Trace_Window(view, current_snapshot, trace)
   }
 
-  private def handle_resize(): Unit = pretty_text_area.zoom()
-
   private def handle_update(follow: Boolean): Unit = {
     val (new_snapshot, new_command, new_results, new_id) =
       PIDE.editor.current_node_snapshot(view) match {
@@ -92,7 +94,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        GUI_Thread.later { handle_resize() }
+        GUI_Thread.later { output.handle_resize() }
 
       case changed: Session.Commands_Changed =>
         GUI_Thread.later { handle_update(do_update) }
@@ -109,6 +111,7 @@
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
     PIDE.session.trace_events += main
+    output.init()
     handle_update(true)
   }
 
@@ -117,21 +120,10 @@
     PIDE.session.commands_changed -= main
     PIDE.session.caret_focus -= main
     PIDE.session.trace_events -= main
-    delay_resize.revoke()
+    output.exit()
   }
 
 
-  /* resize */
-
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-
   /* controls */
 
   private val controls =
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -19,15 +19,19 @@
 
 
 class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
-  /* text area */
+  /* output text area */
+
+  private val output: Output_Area = new Output_Area(view)
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
 
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+  output.setup(dockable)
+  set_content(output.text_pane)
 
 
   /* query operation */
@@ -46,20 +50,8 @@
   }
 
   private val sledgehammer =
-    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, pretty_text_area.update)
-
-
-  /* resize */
-
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
+    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
+      output.pretty_text_area.update)
 
 
   /* controls */
@@ -123,7 +115,7 @@
     Wrap_Panel(
       List(provers_label, Component.wrap(provers), isar_proofs, try0,
         process_indicator.component, apply_query, cancel_query, locate_query,
-        pretty_text_area.zoom_component))
+        output.pretty_text_area.zoom_component))
 
   add(controls.peer, BorderLayout.NORTH)
 
@@ -134,19 +126,20 @@
 
   private val main =
     Session.Consumer[Session.Global_Options](getClass.getName) {
-      case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
+      case _: Session.Global_Options =>
+        GUI_Thread.later { update_provers(); output.handle_resize() }
     }
 
   override def init(): Unit = {
     PIDE.session.global_options += main
     update_provers()
-    handle_resize()
+    output.init()
     sledgehammer.activate()
   }
 
   override def exit(): Unit = {
     sledgehammer.deactivate()
     PIDE.session.global_options -= main
-    delay_resize.revoke()
+    output.exit()
   }
 }
--- a/src/Tools/jEdit/src/state_dockable.scala	Wed Nov 27 16:51:50 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Wed Nov 27 16:52:04 2024 +0100
@@ -16,31 +16,22 @@
 
 
 class State_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
-  /* text area */
+  /* output text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
+  private val output: Output_Area = new Output_Area(view)
 
-  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+  override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation
 
   private val print_state =
-    new Query_Operation(PIDE.editor, view, "print_state", _ => (), pretty_text_area.update)
-
-
-  /* resize */
+    new Query_Operation(PIDE.editor, view, "print_state", _ => (), output.pretty_text_area.update)
 
-  private val delay_resize =
-    Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-  private def handle_resize(): Unit = pretty_text_area.zoom()
+  output.setup(dockable)
+  set_content(output.split_pane)
 
 
   /* update */
@@ -93,7 +84,7 @@
   private val controls =
     Wrap_Panel(
       List(auto_update_button, update_button, locate_button) :::
-      pretty_text_area.search_zoom_components)
+      output.pretty_text_area.search_zoom_components)
 
   add(controls.peer, BorderLayout.NORTH)
 
@@ -103,7 +94,7 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        GUI_Thread.later { handle_resize() }
+        GUI_Thread.later { output.handle_resize() }
 
       case changed: Session.Commands_Changed =>
         if (changed.assignment) GUI_Thread.later { auto_update() }
@@ -116,7 +107,7 @@
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
-    handle_resize()
+    output.init()
     print_state.activate()
     auto_update()
   }
@@ -126,6 +117,6 @@
     PIDE.session.caret_focus -= main
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
-    delay_resize.revoke()
+    output.exit()
   }
 }