1.1 --- a/src/Pure/PIDE/query_operation.scala	Fri Oct 11 12:06:26 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Fri Oct 11 20:45:21 2013 +0200
     1.3 @@ -155,13 +155,15 @@
     1.4          remove_overlay()
     1.5          reset_state()
     1.6          consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
     1.7 -        editor.current_command(editor_context, snapshot) match {
     1.8 -          case Some(command) =>
     1.9 -            current_location = Some(command)
    1.10 -            current_query = query
    1.11 -            current_status = Query_Operation.Status.WAITING
    1.12 -            editor.insert_overlay(command, operation_name, instance :: query)
    1.13 -          case None =>
    1.14 +        if (!snapshot.is_outdated) {
    1.15 +          editor.current_command(editor_context, snapshot) match {
    1.16 +            case Some(command) =>
    1.17 +              current_location = Some(command)
    1.18 +              current_query = query
    1.19 +              current_status = Query_Operation.Status.WAITING
    1.20 +              editor.insert_overlay(command, operation_name, instance :: query)
    1.21 +            case None =>
    1.22 +          }
    1.23          }
    1.24          consume_status(current_status)
    1.25          editor.flush()

     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Oct 11 12:06:26 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Oct 11 20:45:21 2013 +0200
     2.3 @@ -100,10 +100,11 @@
     2.4      Swing_Thread.require()
     2.5  
     2.6      if (Isabelle.continuous_checking) {
     2.7 +      val snapshot = this.snapshot()
     2.8        Document.Node.Perspective(node_required, Text.Perspective(
     2.9          for {
    2.10            doc_view <- PIDE.document_views(buffer)
    2.11 -          range <- doc_view.perspective().ranges
    2.12 +          range <- doc_view.perspective(snapshot).ranges
    2.13          } yield range), PIDE.editor.node_overlays(node_name))
    2.14      }
    2.15      else empty_perspective

     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 11 12:06:26 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 11 20:45:21 2013 +0200
     3.3 @@ -77,14 +77,25 @@
     3.4  
     3.5    /* perspective */
     3.6  
     3.7 -  def perspective(): Text.Perspective =
     3.8 +  def perspective(snapshot: Document.Snapshot): Text.Perspective =
     3.9    {
    3.10      Swing_Thread.require()
    3.11  
    3.12 -    val active_caret =
    3.13 -      if (text_area.getView != null && text_area.getView.getTextArea == text_area)
    3.14 -        List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
    3.15 +    val active_command =
    3.16 +    {
    3.17 +      val view = text_area.getView
    3.18 +      if (view != null && view.getTextArea == text_area) {
    3.19 +        PIDE.editor.current_command(view, snapshot) match {
    3.20 +          case Some(command) =>
    3.21 +            snapshot.node.command_start(command) match {
    3.22 +              case Some(start) => List(command.proper_range + start)
    3.23 +              case None => Nil
    3.24 +            }
    3.25 +          case None => Nil
    3.26 +        }
    3.27 +      }
    3.28        else Nil
    3.29 +    }
    3.30  
    3.31      val buffer_range = JEdit_Lib.buffer_range(model.buffer)
    3.32      val visible_lines =
    3.33 @@ -98,7 +109,7 @@
    3.34        }
    3.35        yield range).toList
    3.36  
    3.37 -    Text.Perspective(active_caret ::: visible_lines)
    3.38 +    Text.Perspective(active_command ::: visible_lines)
    3.39    }
    3.40  
    3.41    private def update_perspective = new TextAreaExtension

     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Oct 11 12:06:26 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Oct 11 20:45:21 2013 +0200
     4.3 @@ -66,24 +66,21 @@
     4.4    {
     4.5      Swing_Thread.require()
     4.6  
     4.7 -    if (snapshot.is_outdated) None
     4.8 -    else {
     4.9 -      val text_area = view.getTextArea
    4.10 -      PIDE.document_view(text_area) match {
    4.11 -        case Some(doc_view) =>
    4.12 -          val node = snapshot.version.nodes(doc_view.model.node_name)
    4.13 -          val caret = text_area.getCaretPosition
    4.14 -          if (caret < text_area.getBuffer.getLength) {
    4.15 -            val caret_commands = node.command_range(caret)
    4.16 -            if (caret_commands.hasNext) {
    4.17 -              val (cmd0, _) = caret_commands.next
    4.18 -              node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    4.19 -            }
    4.20 -            else None
    4.21 +    val text_area = view.getTextArea
    4.22 +    PIDE.document_view(text_area) match {
    4.23 +      case Some(doc_view) =>
    4.24 +        val node = snapshot.version.nodes(doc_view.model.node_name)
    4.25 +        val caret = snapshot.revert(text_area.getCaretPosition)
    4.26 +        if (caret < text_area.getBuffer.getLength) {
    4.27 +          val caret_commands = node.command_range(caret)
    4.28 +          if (caret_commands.hasNext) {
    4.29 +            val (cmd0, _) = caret_commands.next
    4.30 +            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    4.31            }
    4.32 -          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    4.33 -        case None => None
    4.34 -      }
    4.35 +          else None
    4.36 +        }
    4.37 +        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    4.38 +      case None => None
    4.39      }
    4.40    }
    4.41