# HG changeset patch # User wenzelm # Date 1325936386 -3600 # Node ID 793cecd4ffc0628db0fa5da04004f25513bb0728 # Parent 913ea585efdca0b589e8fb30b84288a6ba4a27f9 accumulate status as regular markup for command range; tuned signature; diff -r 913ea585efdc -r 793cecd4ffc0 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Jan 07 11:45:53 2012 +0100 +++ b/src/Pure/PIDE/command.scala Sat Jan 07 12:39:46 2012 +0100 @@ -23,27 +23,20 @@ val results: SortedMap[Long, XML.Tree] = SortedMap.empty, val markup: Markup_Tree = Markup_Tree.empty) { - /* content */ - - def add_status(st: Markup): State = copy(status = st :: status) - def add_markup(m: Text.Markup): State = copy(markup = markup + m) - def add_result(serial: Long, result: XML.Tree): State = - copy(results = results + (serial -> result)) + /* accumulate content */ - def root_info: Text.Markup = - Text.Info(command.range, - XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil)))) - def root_markup: Markup_Tree = markup + root_info + private def add_status(st: Markup): State = copy(status = st :: status) + private def add_markup(m: Text.Markup): State = copy(markup = markup + m) - - /* message dispatch */ - - def accumulate(message: XML.Elem): Command.State = + def + (message: XML.Elem): Command.State = message match { case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) => (this /: msgs)((state, msg) => msg match { - case XML.Elem(markup, Nil) => state.add_status(markup) + case elem @ XML.Elem(markup, Nil) => + val info: Text.Markup = Text.Info(command.range, elem) + state.add_status(markup).add_markup(info) + case _ => System.err.println("Ignored status message: " + msg); state }) @@ -64,13 +57,13 @@ atts match { case Isabelle_Markup.Serial(i) => val result = XML.Elem(Markup(name, Position.purge(atts)), body) - val st0 = add_result(i, result) + val st0 = copy(results = results + (i -> result)) val st1 = if (Protocol.is_tracing(message)) st0 else (st0 /: Protocol.message_positions(command, message))( (st, range) => st.add_markup(Text.Info(range, result))) - val st2 = (st1 /: Protocol.message_reports(message))(_ accumulate _) + val st2 = (st1 /: Protocol.message_reports(message))(_ + _) st2 case _ => System.err.println("Ignored message without serial number: " + message); this } diff -r 913ea585efdc -r 793cecd4ffc0 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Jan 07 11:45:53 2012 +0100 +++ b/src/Pure/PIDE/document.scala Sat Jan 07 12:39:46 2012 +0100 @@ -325,12 +325,12 @@ def accumulate(id: ID, message: XML.Elem): (Command.State, State) = execs.get(id) match { case Some(st) => - val new_st = st.accumulate(message) + val new_st = st + message (new_st, copy(execs = execs + (id -> new_st))) case None => commands.get(id) match { case Some(st) => - val new_st = st.accumulate(message) + val new_st = st + message (new_st, copy(commands = commands + (id -> new_st))) case None => fail } diff -r 913ea585efdc -r 793cecd4ffc0 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 07 11:45:53 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 07 12:39:46 2012 +0100 @@ -152,7 +152,7 @@ val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range() if !stopped) { - snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Markup) => + snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) => { val range = info.range + command_start val content = command.source(info.range).replace('\n', ' ')