# HG changeset patch
# User wenzelm
# Date 1376311996 -7200
# Node ID 37fbb3fde3802af1d5d9fa95ab38b599d2126e6c
# Parent  15254e32d2996df07661c7e67dd2a08af3afd703
prefer PIDE editor operations;
apply_query: insist in non-outdated snapshot via editor.current_command;
tuned signature;

diff -r 15254e32d299 -r 37fbb3fde380 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Aug 12 14:27:58 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 12 14:53:16 2013 +0200
@@ -208,12 +208,6 @@
     def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
       command_range(range.start) takeWhile { case (_, start) => start < range.stop }
 
-    def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
-    {
-      val range = command_range(i)
-      if (range.hasNext) Some(range.next) else None
-    }
-
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
   }
diff -r 15254e32d299 -r 37fbb3fde380 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Aug 12 14:27:58 2013 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 14:53:16 2013 +0200
@@ -13,7 +13,7 @@
   def flush(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]
-  def current_snapshot(context: Context): Option[Document.Snapshot]
+  def current_node_snapshot(context: Context): Option[Document.Snapshot]
   def node_snapshot(name: Document.Node.Name): Document.Snapshot
   def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
 
diff -r 15254e32d299 -r 37fbb3fde380 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:27:58 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:53:16 2013 +0200
@@ -45,7 +45,7 @@
   def current_node(view: View): Option[Document.Node.Name] =
     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
 
-  def current_snapshot(view: View): Option[Document.Snapshot] =
+  def current_node_snapshot(view: View): Option[Document.Snapshot] =
     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
 
   def node_snapshot(name: Document.Node.Name): Document.Snapshot =
@@ -72,7 +72,8 @@
       PIDE.document_view(text_area) match {
         case Some(doc_view) =>
           val node = snapshot.version.nodes(doc_view.model.node_name)
-          node.command_at(text_area.getCaretPosition)
+          val caret_commands = node.command_range(text_area.getCaretPosition)
+          if (caret_commands.hasNext) Some(caret_commands.next) else None
         case None => None
       }
     }
diff -r 15254e32d299 -r 37fbb3fde380 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Aug 12 14:27:58 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Aug 12 14:53:16 2013 +0200
@@ -54,12 +54,11 @@
     Swing_Thread.require()
 
     val (new_snapshot, new_state) =
-      Document_View(view.getTextArea) match {
-        case Some(doc_view) =>
-          val snapshot = doc_view.model.snapshot()
+      PIDE.editor.current_node_snapshot(view) match {
+        case Some(snapshot) =>
           if (follow && !snapshot.is_outdated) {
-            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
-              case Some(cmd) =>
+            PIDE.editor.current_command(view, snapshot) match {
+              case Some((cmd, _)) =>
                 (snapshot, snapshot.state.command_state(snapshot.version, cmd))
               case None =>
                 (Document.Snapshot.init, Command.empty.init_state)
diff -r 15254e32d299 -r 37fbb3fde380 src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 14:27:58 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 14:53:16 2013 +0200
@@ -151,14 +151,13 @@
   {
     Swing_Thread.require()
 
-    Document_View(view.getTextArea) match {
-      case Some(doc_view) =>
-        val snapshot = doc_view.model.snapshot()
+    editor.current_node_snapshot(view) match {
+      case Some(snapshot) =>
         remove_overlay()
         reset_state()
         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
-        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
-          case Some(command) =>
+        editor.current_command(view, snapshot) match {
+          case Some((command, _)) =>
             current_location = Some(command)
             current_query = query
             current_status = Query_Operation.Status.WAITING