clarified valid_id: always standardize towards static command.id;
authorwenzelm
Wed Mar 26 19:42:16 2014 +0100 (2014-03-26)
changeset 56295a40e67ce4f84
parent 56294 85911b8a6868
child 56296 5413b6379c0e
clarified valid_id: always standardize towards static command.id;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Mar 26 14:41:52 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Mar 26 19:42:16 2014 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4        copy(markups = markups1.add(Markup_Index(false, file_name), m))
     1.5      }
     1.6  
     1.7 -    def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
     1.8 +    def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
     1.9        message match {
    1.10          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    1.11            (this /: msgs)((state, msg) =>
    1.12 @@ -154,7 +154,7 @@
    1.13                msg match {
    1.14                  case XML.Elem(Markup(name,
    1.15                    atts @ Position.Reported(id, file_name, symbol_range)), args)
    1.16 -                if id == command.id || id == alt_id =>
    1.17 +                if valid_id(id) =>
    1.18                    command.chunks.get(file_name) match {
    1.19                      case Some(chunk) =>
    1.20                        chunk.incorporate(symbol_range) match {
    1.21 @@ -187,7 +187,7 @@
    1.22                if (Protocol.is_inlined(message)) {
    1.23                  for {
    1.24                    (file_name, chunk) <- command.chunks
    1.25 -                  range <- Protocol.message_positions(command.id, alt_id, chunk, message)
    1.26 +                  range <- Protocol.message_positions(valid_id, chunk, message)
    1.27                  } st = st.add_markup(false, file_name, Text.Info(range, message2))
    1.28                }
    1.29                st
    1.30 @@ -196,7 +196,7 @@
    1.31                System.err.println("Ignored message without serial number: " + message)
    1.32                this
    1.33            }
    1.34 -      }
    1.35 +    }
    1.36  
    1.37      def ++ (other: State): State =
    1.38        copy(
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 26 14:41:52 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Mar 26 19:42:16 2014 +0100
     2.3 @@ -521,15 +521,19 @@
     2.4      def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     2.5      def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
     2.6  
     2.7 +    def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
     2.8 +      id == st.command.id ||
     2.9 +      (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
    2.10 +
    2.11      def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
    2.12        execs.get(id) match {
    2.13          case Some(st) =>
    2.14 -          val new_st = st + (id, message)
    2.15 +          val new_st = st + (valid_id(st), message)
    2.16            (new_st, copy(execs = execs + (id -> new_st)))
    2.17          case None =>
    2.18            commands.get(id) match {
    2.19              case Some(st) =>
    2.20 -              val new_st = st + (id, message)
    2.21 +              val new_st = st + (valid_id(st), message)
    2.22                (new_st, copy(commands = commands + (id -> new_st)))
    2.23              case None => fail
    2.24            }
     3.1 --- a/src/Pure/PIDE/protocol.scala	Wed Mar 26 14:41:52 2014 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Mar 26 19:42:16 2014 +0100
     3.3 @@ -280,15 +280,14 @@
     3.4      Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     3.5  
     3.6    def message_positions(
     3.7 -    command_id: Document_ID.Command,
     3.8 -    alt_id: Document_ID.Generic,
     3.9 +    valid_id: Document_ID.Generic => Boolean,
    3.10      chunk: Command.Chunk,
    3.11      message: XML.Elem): Set[Text.Range] =
    3.12    {
    3.13      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
    3.14        props match {
    3.15          case Position.Reported(id, file_name, symbol_range)
    3.16 -        if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
    3.17 +        if valid_id(id) && file_name == chunk.file_name =>
    3.18            chunk.incorporate(symbol_range) match {
    3.19              case Some(range) => set + range
    3.20              case _ => set