Command.results: ordered by serial number;
authorwenzelm
Mon Aug 30 13:01:32 2010 +0200 (2010-08-30)
changeset 3887226c505765024
parent 38871 28496da3bec2
child 38873 278f552b2e97
Command.results: ordered by serial number;
src/Pure/General/markup.scala
src/Pure/General/position.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
     1.1 --- a/src/Pure/General/markup.scala	Mon Aug 30 11:35:17 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Mon Aug 30 13:01:32 2010 +0200
     1.3 @@ -226,7 +226,7 @@
     1.4    /* messages */
     1.5  
     1.6    val PID = "pid"
     1.7 -  val SERIAL = "serial"
     1.8 +  val Serial = new Long_Property("serial")
     1.9  
    1.10    val MESSAGE = "message"
    1.11    val CLASS = "class"
     2.1 --- a/src/Pure/General/position.scala	Mon Aug 30 11:35:17 2010 +0200
     2.2 +++ b/src/Pure/General/position.scala	Mon Aug 30 13:01:32 2010 +0200
     2.3 @@ -28,4 +28,6 @@
     2.4          case _ => None
     2.5        }
     2.6    }
     2.7 +
     2.8 +  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
     2.9  }
     3.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 30 11:35:17 2010 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Mon Aug 30 13:01:32 2010 +0200
     3.3 @@ -8,23 +8,25 @@
     3.4  package isabelle
     3.5  
     3.6  
     3.7 +import scala.collection.immutable.SortedMap
     3.8 +
     3.9 +
    3.10  object Command
    3.11  {
    3.12    /** accumulated results from prover **/
    3.13  
    3.14    case class State(
    3.15      val command: Command,
    3.16 -    val status: List[Markup],
    3.17 -    val reverse_results: List[XML.Tree],
    3.18 -    val markup: Markup_Tree)
    3.19 +    val status: List[Markup] = Nil,
    3.20 +    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
    3.21 +    val markup: Markup_Tree = Markup_Tree.empty)
    3.22    {
    3.23      /* content */
    3.24  
    3.25 -    lazy val results = reverse_results.reverse
    3.26 -
    3.27      def add_status(st: Markup): State = copy(status = st :: status)
    3.28      def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
    3.29 -    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    3.30 +    def add_result(serial: Long, result: XML.Tree): State =
    3.31 +      copy(results = results + (serial -> result))
    3.32  
    3.33      def root_info: Text.Info[Any] =
    3.34        new Text.Info(command.range,
    3.35 @@ -34,7 +36,7 @@
    3.36  
    3.37      /* message dispatch */
    3.38  
    3.39 -    def accumulate(message: XML.Tree): Command.State =
    3.40 +    def accumulate(message: XML.Elem): Command.State =
    3.41        message match {
    3.42          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    3.43            (this /: msgs)((state, msg) =>
    3.44 @@ -48,13 +50,18 @@
    3.45              msg match {
    3.46                case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
    3.47                if Position.Id.unapply(atts) == Some(command.id) =>
    3.48 -                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    3.49 +                val props = Position.purge(atts)
    3.50                  val info =
    3.51                    Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
    3.52                  state.add_markup(info)
    3.53                case _ => System.err.println("Ignored report message: " + msg); state
    3.54              })
    3.55 -        case _ => add_result(message)
    3.56 +        case XML.Elem(Markup(name, atts), body) =>
    3.57 +          atts match {
    3.58 +            case Markup.Serial(i) =>
    3.59 +              add_result(i, XML.Elem(Markup(name, Position.purge(atts)), body))
    3.60 +            case _ => System.err.println("Ignored message without serial number: " + message); this
    3.61 +          }
    3.62        }
    3.63    }
    3.64  
    3.65 @@ -98,5 +105,5 @@
    3.66  
    3.67    /* accumulated results */
    3.68  
    3.69 -  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
    3.70 +  val empty_state: Command.State = Command.State(this)
    3.71  }
     4.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 30 11:35:17 2010 +0200
     4.2 +++ b/src/Pure/PIDE/document.scala	Mon Aug 30 13:01:32 2010 +0200
     4.3 @@ -204,7 +204,7 @@
     4.4      def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
     4.5      def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
     4.6  
     4.7 -    def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
     4.8 +    def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
     4.9        execs.get(id) match {
    4.10          case Some((st, occs)) =>
    4.11            val new_st = st.accumulate(message)
     5.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 30 11:35:17 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Aug 30 13:01:32 2010 +0200
     5.3 @@ -67,12 +67,12 @@
     5.4              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
     5.5                val snapshot = doc_view.model.snapshot()
     5.6                val filtered_results =
     5.7 -                snapshot.state(cmd).results filter {
     5.8 +                snapshot.state(cmd).results.iterator.map(_._2) filter {
     5.9                    case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
    5.10                    case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
    5.11                    case _ => true
    5.12                  }
    5.13 -              html_panel.render(filtered_results)
    5.14 +              html_panel.render(filtered_results.toList)
    5.15              case _ =>
    5.16            }
    5.17          case None =>