# HG changeset patch
# User wenzelm
# Date 1753713235 -7200
# Node ID cfc15a2c1f1e31712c8b5fe614ddb1965a8c71e5
# Parent  75e7ca688f608b9abc2fb166b8734d62b5e09631
more uniform JEdit_Editor.current_command wrt. PIDE document and Isabelle/VSCode (see also 842adea880a4 and 6bd7081f8319);

diff -r 75e7ca688f60 -r cfc15a2c1f1e src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Jul 28 16:14:46 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Jul 28 16:33:55 2025 +0200
@@ -78,23 +78,15 @@
   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
     GUI_Thread.require { Document_Model.get_snapshot(name) getOrElse session.snapshot(name) }
 
-  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = {
-    GUI_Thread.require {}
-
-    val text_area = view.getTextArea
-    val buffer = view.getBuffer
-
-    Document_View.get(text_area) match {
-      case Some(doc_view) if doc_view.model.is_theory =>
-        snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
-      case _ =>
-        Document_Model.get_model(buffer) match {
-          case Some(model) if !model.is_theory =>
-            snapshot.version.nodes.commands_loading(model.node_name).headOption
-          case _ => None
-        }
+  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
+    GUI_Thread.require {
+      val text_area = view.getTextArea
+      Document_View.get(text_area) match {
+        case Some(doc_view) =>
+          snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
+        case None => None
+      }
     }
-  }
 
 
   /* overlays */