--- a/src/Pure/PIDE/editor.scala Tue Dec 20 22:24:36 2022 +0000
+++ b/src/Pure/PIDE/editor.scala Wed Dec 21 11:30:24 2022 +0100
@@ -27,7 +27,10 @@
val changed =
document_editor.change_result { st =>
val st1 = f(st)
- (st.required != st1.required, st1)
+ val changed =
+ st.active_document_theories != st1.active_document_theories ||
+ st.required != st1.required
+ (changed, st1)
}
if (changed) document_state_changed()
}
--- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 22:24:36 2022 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 11:30:24 2022 +0100
@@ -160,8 +160,7 @@
finish_process(Nil)
GUI_Thread.later {
- val domain = PIDE.editor.document_theories().toSet
- theories.update(domain = Some(domain), trim = true, force = true)
+ refresh_theories()
show_state()
show_page(theories_page)
}
@@ -267,6 +266,12 @@
private val theories = new Theories_Status(view, document = true)
+ private def refresh_theories(): Unit = {
+ val domain = PIDE.editor.document_theories().toSet
+ theories.update(domain = Some(domain), trim = true, force = true)
+ theories.refresh()
+ }
+
private val theories_page =
new TabbedPane.Page("Theories", new BorderPanel {
layout(theories_controls) = BorderPanel.Position.North
@@ -300,7 +305,7 @@
GUI_Thread.later {
document_session.load()
handle_resize()
- theories.refresh()
+ refresh_theories()
}
case changed: Session.Commands_Changed =>
GUI_Thread.later {