1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 11 22:41:26 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 11 23:29:17 2010 +0200
     1.3 @@ -101,6 +101,7 @@
     1.4      val is_outdated: Boolean
     1.5      def convert(offset: Int): Int
     1.6      def revert(offset: Int): Int
     1.7 +    def state(command: Command): State
     1.8    }
     1.9  
    1.10    object Change
    1.11 @@ -145,6 +146,7 @@
    1.12          val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
    1.13          def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    1.14          def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.15 +        def state(command: Command): State = document.current_state(command)
    1.16        }
    1.17      }
    1.18    }

     2.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Aug 11 22:41:26 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Aug 11 23:29:17 2010 +0200
     2.3 @@ -278,7 +278,7 @@
     2.4        for {
     2.5          (command, command_start) <-
     2.6            snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
     2.7 -        markup <- snapshot.document.current_state(command).highlight.flatten
     2.8 +        markup <- snapshot.state(command).highlight.flatten
     2.9          val abs_start = snapshot.convert(command_start + markup.start)
    2.10          val abs_stop = snapshot.convert(command_start + markup.stop)
    2.11          if (abs_stop > start)

     3.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed Aug 11 22:41:26 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Aug 11 23:29:17 2010 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4  {
     3.5    def choose_color(snapshot: Document.Snapshot, command: Command): Color =
     3.6    {
     3.7 -    val state = snapshot.document.current_state(command)
     3.8 +    val state = snapshot.state(command)
     3.9      if (snapshot.is_outdated) new Color(240, 240, 240)
    3.10      else if (state.forks > 0) new Color(255, 228, 225)
    3.11      else if (state.forks < 0) Color.red
    3.12 @@ -203,7 +203,7 @@
    3.13        val offset = snapshot.revert(text_area.xyToOffset(x, y))
    3.14        snapshot.node.command_at(offset) match {
    3.15          case Some((command, command_start)) =>
    3.16 -          snapshot.document.current_state(command).type_at(offset - command_start) match {
    3.17 +          snapshot.state(command).type_at(offset - command_start) match {
    3.18              case Some(text) => Isabelle.tooltip(text)
    3.19              case None => null
    3.20            }

     4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 11 22:41:26 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Aug 11 23:29:17 2010 +0200
     4.3 @@ -47,7 +47,7 @@
     4.4          val offset = snapshot.revert(original_offset)
     4.5          snapshot.node.command_at(offset) match {
     4.6            case Some((command, command_start)) =>
     4.7 -            snapshot.document.current_state(command).ref_at(offset - command_start) match {
     4.8 +            snapshot.state(command).ref_at(offset - command_start) match {
     4.9                case Some(ref) =>
    4.10                  val begin = snapshot.convert(command_start + ref.start)
    4.11                  val line = buffer.getLineOfOffset(begin)

     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 11 22:41:26 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Aug 11 23:29:17 2010 +0200
     5.3 @@ -130,7 +130,7 @@
     5.4      val root = data.root
     5.5      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     5.6      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
     5.7 -      root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
     5.8 +      root.add(snapshot.state(command).markup_root.swing_tree((node: Markup_Node) =>
     5.9            {
    5.10              val content = command.source(node.start, node.stop).replace('\n', ' ')
    5.11              val id = command.id

     6.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Aug 11 22:41:26 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Aug 11 23:29:17 2010 +0200
     6.3 @@ -67,7 +67,7 @@
     6.4              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
     6.5                val snapshot = doc_view.model.snapshot()
     6.6                val filtered_results =
     6.7 -                snapshot.document.current_state(cmd).results filter {
     6.8 +                snapshot.state(cmd).results filter {
     6.9                    case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
    6.10                    case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
    6.11                    case _ => true