# HG changeset patch
# User wenzelm
# Date 1381517121 -7200
# Node ID 2c4155003352be3d9c0990f2ec3f328426418cfd
# Parent  dabaf9ca15132b01735824c76fd4b65a546a85c6
clarified Editor.current_command: allow outdated snapshot;
more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);

diff -r dabaf9ca1513 -r 2c4155003352 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Fri Oct 11 12:06:26 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Fri Oct 11 20:45:21 2013 +0200
@@ -155,13 +155,15 @@
         remove_overlay()
         reset_state()
         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
-        editor.current_command(editor_context, snapshot) match {
-          case Some(command) =>
-            current_location = Some(command)
-            current_query = query
-            current_status = Query_Operation.Status.WAITING
-            editor.insert_overlay(command, operation_name, instance :: query)
-          case None =>
+        if (!snapshot.is_outdated) {
+          editor.current_command(editor_context, snapshot) match {
+            case Some(command) =>
+              current_location = Some(command)
+              current_query = query
+              current_status = Query_Operation.Status.WAITING
+              editor.insert_overlay(command, operation_name, instance :: query)
+            case None =>
+          }
         }
         consume_status(current_status)
         editor.flush()
diff -r dabaf9ca1513 -r 2c4155003352 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Oct 11 12:06:26 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Oct 11 20:45:21 2013 +0200
@@ -100,10 +100,11 @@
     Swing_Thread.require()
 
     if (Isabelle.continuous_checking) {
+      val snapshot = this.snapshot()
       Document.Node.Perspective(node_required, Text.Perspective(
         for {
           doc_view <- PIDE.document_views(buffer)
-          range <- doc_view.perspective().ranges
+          range <- doc_view.perspective(snapshot).ranges
         } yield range), PIDE.editor.node_overlays(node_name))
     }
     else empty_perspective
diff -r dabaf9ca1513 -r 2c4155003352 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 11 12:06:26 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 11 20:45:21 2013 +0200
@@ -77,14 +77,25 @@
 
   /* perspective */
 
-  def perspective(): Text.Perspective =
+  def perspective(snapshot: Document.Snapshot): Text.Perspective =
   {
     Swing_Thread.require()
 
-    val active_caret =
-      if (text_area.getView != null && text_area.getView.getTextArea == text_area)
-        List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
+    val active_command =
+    {
+      val view = text_area.getView
+      if (view != null && view.getTextArea == text_area) {
+        PIDE.editor.current_command(view, snapshot) match {
+          case Some(command) =>
+            snapshot.node.command_start(command) match {
+              case Some(start) => List(command.proper_range + start)
+              case None => Nil
+            }
+          case None => Nil
+        }
+      }
       else Nil
+    }
 
     val buffer_range = JEdit_Lib.buffer_range(model.buffer)
     val visible_lines =
@@ -98,7 +109,7 @@
       }
       yield range).toList
 
-    Text.Perspective(active_caret ::: visible_lines)
+    Text.Perspective(active_command ::: visible_lines)
   }
 
   private def update_perspective = new TextAreaExtension
diff -r dabaf9ca1513 -r 2c4155003352 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Oct 11 12:06:26 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Oct 11 20:45:21 2013 +0200
@@ -66,24 +66,21 @@
   {
     Swing_Thread.require()
 
-    if (snapshot.is_outdated) None
-    else {
-      val text_area = view.getTextArea
-      PIDE.document_view(text_area) match {
-        case Some(doc_view) =>
-          val node = snapshot.version.nodes(doc_view.model.node_name)
-          val caret = text_area.getCaretPosition
-          if (caret < text_area.getBuffer.getLength) {
-            val caret_commands = node.command_range(caret)
-            if (caret_commands.hasNext) {
-              val (cmd0, _) = caret_commands.next
-              node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
-            }
-            else None
+    val text_area = view.getTextArea
+    PIDE.document_view(text_area) match {
+      case Some(doc_view) =>
+        val node = snapshot.version.nodes(doc_view.model.node_name)
+        val caret = snapshot.revert(text_area.getCaretPosition)
+        if (caret < text_area.getBuffer.getLength) {
+          val caret_commands = node.command_range(caret)
+          if (caret_commands.hasNext) {
+            val (cmd0, _) = caret_commands.next
+            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
           }
-          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
-        case None => None
-      }
+          else None
+        }
+        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
+      case None => None
     }
   }