more uniform JEdit_Editor.current_command wrt. PIDE document and Isabelle/VSCode (see also 842adea880a4 and 6bd7081f8319);
--- 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 */