# HG changeset patch
# User wenzelm
# Date 1743424366 -7200
# Node ID 8f83f798d46795863576113004c887a4c1b7ab6f
# Parent  3118a565865815419de14f35aeee338f697066f7
misc tuning: more modular message dispatch;

diff -r 3118a5658658 -r 8f83f798d467 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Mar 29 15:35:12 2025 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Mon Mar 31 14:32:46 2025 +0200
@@ -301,17 +301,18 @@
     if (startup_failure.isEmpty) {
       message match {
         case _: EditorStarted =>
+          val view = jEdit.getActiveView
+
           try { resources.session_background.check_errors }
           catch {
             case ERROR(msg) =>
-              GUI.warning_dialog(jEdit.getActiveView,
+              GUI.warning_dialog(view,
                 "Bad session structure: may cause problems with theory imports",
                 GUI.scrollable_text(msg))
           }
 
           jEdit.propertiesChanged()
 
-          val view = jEdit.getActiveView
           if (view != null) {
             init_editor(view)
 
@@ -319,49 +320,46 @@
               JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
           }
 
-        case msg: ViewUpdate
-        if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
-          init_title(msg.getView)
-
-        case msg: BufferUpdate
-        if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
-          if (msg.getBuffer != null) {
-            exit_models(List(msg.getBuffer))
-            PIDE.editor.invoke_generated()
+        case msg: ViewUpdate =>
+          val what = msg.getWhat
+          val view = msg.getView
+          what match {
+            case ViewUpdate.CREATED if view != null => init_title(view)
+            case _ =>
           }
 
-        case msg: BufferUpdate
-        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
-          if (session.is_ready) {
-            delay_init.invoke()
-            delay_load.invoke()
+        case msg: BufferUpdate =>
+          val what = msg.getWhat
+          val buffer = msg.getBuffer
+          what match {
+            case BufferUpdate.LOAD_STARTED | BufferUpdate.CLOSING if buffer != null =>
+              exit_models(List(buffer))
+              PIDE.editor.invoke_generated()
+            case BufferUpdate.PROPERTIES_CHANGED | BufferUpdate.LOADED if session.is_ready =>
+              delay_init.invoke()
+              delay_load.invoke()
+            case _ =>
           }
 
-        case msg: EditPaneUpdate
-        if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
-            msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
-            msg.getWhat == EditPaneUpdate.CREATED ||
-            msg.getWhat == EditPaneUpdate.DESTROYED =>
+        case msg: EditPaneUpdate =>
+          val what = msg.getWhat
           val edit_pane = msg.getEditPane
-          val buffer = edit_pane.getBuffer
-          val text_area = edit_pane.getTextArea
+          val buffer = if (edit_pane == null) null else edit_pane.getBuffer
+          val text_area = if (edit_pane == null) null else edit_pane.getTextArea
 
           if (buffer != null && text_area != null) {
-            if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
-                msg.getWhat == EditPaneUpdate.CREATED) {
-              if (session.is_ready)
-                init_view(buffer, text_area)
+            if (what == EditPaneUpdate.BUFFER_CHANGED || what == EditPaneUpdate.CREATED) {
+              if (session.is_ready) init_view(buffer, text_area)
             }
-            else {
+
+            if (what == EditPaneUpdate.BUFFER_CHANGING || what == EditPaneUpdate.DESTROYED) {
               Isabelle.dismissed_popups(text_area.getView)
               exit_view(buffer, text_area)
             }
 
-            if (msg.getWhat == EditPaneUpdate.CREATED)
-              Completion_Popup.Text_Area.init(text_area)
+            if (what == EditPaneUpdate.CREATED) Completion_Popup.Text_Area.init(text_area)
 
-            if (msg.getWhat == EditPaneUpdate.DESTROYED)
-              Completion_Popup.Text_Area.exit(text_area)
+            if (what == EditPaneUpdate.DESTROYED) Completion_Popup.Text_Area.exit(text_area)
           }
 
         case _: PropertiesChanged =>