tuned signature;
authorwenzelm
Sat Jan 14 15:20:29 2012 +0100 (2012-01-14 ago)
changeset 462084cab63a6dc16
parent 46207 e76b77356ed6
child 46209 aad604f74be0
tuned signature;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/output_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Jan 14 14:34:42 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Jan 14 15:20:29 2012 +0100
     1.3 @@ -234,7 +234,6 @@
     1.4      val version: Version
     1.5      val node: Node
     1.6      val is_outdated: Boolean
     1.7 -    def command_state(command: Command): Command.State
     1.8      def convert(i: Text.Offset): Text.Offset
     1.9      def convert(range: Text.Range): Text.Range
    1.10      def revert(i: Text.Offset): Text.Offset
    1.11 @@ -465,7 +464,6 @@
    1.12          val version = stable.version.get_finished
    1.13          val node = version.nodes(name)
    1.14          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.15 -        def command_state(command: Command): Command.State = state.command_state(version, command)
    1.16  
    1.17          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.18          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.19 @@ -478,7 +476,7 @@
    1.20            val former_range = revert(range)
    1.21            for {
    1.22              (command, command_start) <- node.command_range(former_range).toStream
    1.23 -            Text.Info(r0, a) <- command_state(command).markup.
    1.24 +            Text.Info(r0, a) <- state.command_state(version, command).markup.
    1.25                cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
    1.26                  {
    1.27                    case (a, Text.Info(r0, b))
     2.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Jan 14 14:34:42 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Jan 14 15:20:29 2012 +0100
     2.3 @@ -58,9 +58,9 @@
     2.4  
     2.5    def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
     2.6    {
     2.7 -    val state = snapshot.command_state(command)
     2.8      if (snapshot.is_outdated) None
     2.9      else {
    2.10 +      val state = snapshot.state.command_state(snapshot.version, command)
    2.11        val status = Protocol.command_status(state.status)
    2.12  
    2.13        if (status.is_unprocessed) Some(unprocessed_color)
     3.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 14 14:34:42 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 14 15:20:29 2012 +0100
     3.3 @@ -152,7 +152,8 @@
     3.4      val root = data.root
     3.5      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     3.6      for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     3.7 -      snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) =>
     3.8 +      snapshot.state.command_state(snapshot.version, command).markup
     3.9 +        .swing_tree(root)((info: Text.Markup) =>
    3.10            {
    3.11              val range = info.range + command_start
    3.12              val content = command.source(info.range).replace('\n', ' ')
     4.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Sat Jan 14 14:34:42 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Jan 14 15:20:29 2012 +0100
     4.3 @@ -86,11 +86,13 @@
     4.4              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
     4.5                val snapshot = doc_view.update_snapshot()
     4.6                val filtered_results =
     4.7 -                snapshot.command_state(cmd).results.iterator.map(_._2) filter {
     4.8 -                  case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
     4.9 -                  case _ => true
    4.10 -                }
    4.11 -              html_panel.render(filtered_results.toList)
    4.12 +                snapshot.state.command_state(snapshot.version, cmd).results.iterator
    4.13 +                  .map(_._2).filter(
    4.14 +                  { // FIXME not scalable
    4.15 +                    case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
    4.16 +                    case _ => true
    4.17 +                  }).toList
    4.18 +              html_panel.render(filtered_results)
    4.19              case _ =>
    4.20            }
    4.21          case None =>