more uniform JEdit_Editor.current_command wrt. PIDE document and Isabelle/VSCode (see also 842adea880a4 and 6bd7081f8319);
authorwenzelm
Mon, 28 Jul 2025 16:33:55 +0200
changeset 82921 cfc15a2c1f1e
parent 82920 75e7ca688f60
child 82922 b07201796c1e
more uniform JEdit_Editor.current_command wrt. PIDE document and Isabelle/VSCode (see also 842adea880a4 and 6bd7081f8319);
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 */