accumulate under exec_id as well;
authorwenzelm
Sat Sep 22 19:23:04 2012 +0200 (2012-09-22 ago)
changeset 49527b96e4a39cc3e
parent 49526 6d1465c00f2e
child 49528 789b73fcca72
accumulate under exec_id as well;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Sep 22 19:16:48 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Sep 22 19:23:04 2012 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4      private def add_status(st: Markup): State = copy(status = st :: status)
     1.5      private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
     1.6  
     1.7 -    def + (message: XML.Elem): Command.State =
     1.8 +    def + (alt_id: Document.ID, message: XML.Elem): Command.State =
     1.9        message match {
    1.10          case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
    1.11            (this /: msgs)((state, msg) =>
    1.12 @@ -43,7 +43,8 @@
    1.13            (this /: msgs)((state, msg) =>
    1.14              msg match {
    1.15                case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
    1.16 -              if id == command.id && command.range.contains(command.decode(raw_range)) =>
    1.17 +              if (id == command.id || id == alt_id) &&
    1.18 +                  command.range.contains(command.decode(raw_range)) =>
    1.19                  val range = command.decode(raw_range)
    1.20                  val props = Position.purge(atts)
    1.21                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Sep 22 19:16:48 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Sep 22 19:23:04 2012 +0200
     2.3 @@ -373,12 +373,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 + message
     2.8 +          val new_st = st + (id, 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 + message
    2.14 +              val new_st = st + (id, message)
    2.15                (new_st, copy(commands = commands + (id -> new_st)))
    2.16              case None => fail
    2.17            }