accumulate status as regular markup for command range;
authorwenzelm
Sat Jan 07 12:39:46 2012 +0100 (2012-01-07 ago)
changeset 46152793cecd4ffc0
parent 46151 913ea585efdc
child 46153 7e4a18db7384
accumulate status as regular markup for command range;
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Jan 07 11:45:53 2012 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Jan 07 12:39:46 2012 +0100
     1.3 @@ -23,27 +23,20 @@
     1.4      val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     1.5      val markup: Markup_Tree = Markup_Tree.empty)
     1.6    {
     1.7 -    /* content */
     1.8 -
     1.9 -    def add_status(st: Markup): State = copy(status = st :: status)
    1.10 -    def add_markup(m: Text.Markup): State = copy(markup = markup + m)
    1.11 -    def add_result(serial: Long, result: XML.Tree): State =
    1.12 -      copy(results = results + (serial -> result))
    1.13 +    /* accumulate content */
    1.14  
    1.15 -    def root_info: Text.Markup =
    1.16 -      Text.Info(command.range,
    1.17 -        XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
    1.18 -    def root_markup: Markup_Tree = markup + root_info
    1.19 +    private def add_status(st: Markup): State = copy(status = st :: status)
    1.20 +    private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
    1.21  
    1.22 -
    1.23 -    /* message dispatch */
    1.24 -
    1.25 -    def accumulate(message: XML.Elem): Command.State =
    1.26 +    def + (message: XML.Elem): Command.State =
    1.27        message match {
    1.28          case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
    1.29            (this /: msgs)((state, msg) =>
    1.30              msg match {
    1.31 -              case XML.Elem(markup, Nil) => state.add_status(markup)
    1.32 +              case elem @ XML.Elem(markup, Nil) =>
    1.33 +                val info: Text.Markup = Text.Info(command.range, elem)
    1.34 +                state.add_status(markup).add_markup(info)
    1.35 +
    1.36                case _ => System.err.println("Ignored status message: " + msg); state
    1.37              })
    1.38  
    1.39 @@ -64,13 +57,13 @@
    1.40            atts match {
    1.41              case Isabelle_Markup.Serial(i) =>
    1.42                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
    1.43 -              val st0 = add_result(i, result)
    1.44 +              val st0 = copy(results = results + (i -> result))
    1.45                val st1 =
    1.46                  if (Protocol.is_tracing(message)) st0
    1.47                  else
    1.48                    (st0 /: Protocol.message_positions(command, message))(
    1.49                      (st, range) => st.add_markup(Text.Info(range, result)))
    1.50 -              val st2 = (st1 /: Protocol.message_reports(message))(_ accumulate _)
    1.51 +              val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
    1.52                st2
    1.53              case _ => System.err.println("Ignored message without serial number: " + message); this
    1.54            }
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Jan 07 11:45:53 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Jan 07 12:39:46 2012 +0100
     2.3 @@ -325,12 +325,12 @@
     2.4      def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
     2.5        execs.get(id) match {
     2.6          case Some(st) =>
     2.7 -          val new_st = st.accumulate(message)
     2.8 +          val new_st = st + message
     2.9            (new_st, copy(execs = execs + (id -> new_st)))
    2.10          case None =>
    2.11            commands.get(id) match {
    2.12              case Some(st) =>
    2.13 -              val new_st = st.accumulate(message)
    2.14 +              val new_st = st + message
    2.15                (new_st, copy(commands = commands + (id -> new_st)))
    2.16              case None => fail
    2.17            }
     3.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 07 11:45:53 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Jan 07 12:39:46 2012 +0100
     3.3 @@ -152,7 +152,7 @@
     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).root_markup.swing_tree(root)((info: Text.Markup) =>
     3.8 +      snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) =>
     3.9            {
    3.10              val range = info.range + command_start
    3.11              val content = command.source(info.range).replace('\n', ' ')