accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
authorwenzelm
Tue Apr 08 19:17:28 2014 +0200 (2014-04-08)
changeset 564708eda56033203
parent 56469 ffc94a271633
child 56471 2293a4350716
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 16:07:02 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 19:17:28 2014 +0200
     1.3 @@ -81,6 +81,17 @@
     1.4      def add(index: Markup_Index, markup: Text.Markup): Markups =
     1.5        new Markups(rep + (index -> (this(index) + markup)))
     1.6  
     1.7 +    def other_id_iterator: Iterator[Document_ID.Generic] =
     1.8 +      for (Markup_Index(_, Text.Chunk.Id(other_id)) <- rep.keysIterator)
     1.9 +        yield other_id
    1.10 +
    1.11 +    def retarget(other_id: Document_ID.Generic): Markups =
    1.12 +      new Markups(
    1.13 +        (for {
    1.14 +          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    1.15 +          if other_id == id
    1.16 +        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
    1.17 +
    1.18      override def hashCode: Int = rep.hashCode
    1.19      override def equals(that: Any): Boolean =
    1.20        that match {
    1.21 @@ -124,6 +135,9 @@
    1.22  
    1.23      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.24  
    1.25 +    def retarget(other_command: Command): State =
    1.26 +      new State(other_command, Nil, Results.empty, markups.retarget(other_command.id))
    1.27 +
    1.28  
    1.29      def eq_content(other: State): Boolean =
    1.30        command.source == other.command.source &&
    1.31 @@ -143,7 +157,10 @@
    1.32        copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
    1.33      }
    1.34  
    1.35 -    def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
    1.36 +    def accumulate(
    1.37 +        self_id: Document_ID.Generic => Boolean,
    1.38 +        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
    1.39 +        message: XML.Elem): State =
    1.40        message match {
    1.41          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    1.42            (this /: msgs)((state, msg) =>
    1.43 @@ -163,19 +180,25 @@
    1.44                def bad(): Unit = System.err.println("Ignored report message: " + msg)
    1.45  
    1.46                msg match {
    1.47 -                case XML.Elem(Markup(name,
    1.48 -                  atts @ Position.Reported(id, chunk_name, symbol_range)), args)
    1.49 -                if valid_id(id) =>
    1.50 -                  command.chunks.get(chunk_name) match {
    1.51 -                    case Some(chunk) =>
    1.52 -                      chunk.incorporate(symbol_range) match {
    1.53 +                case XML.Elem(
    1.54 +                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
    1.55 +
    1.56 +                  val target =
    1.57 +                    if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
    1.58 +                      Some((chunk_name, command.chunks(chunk_name)))
    1.59 +                    else if (chunk_name == Text.Chunk.Default) other_id(id)
    1.60 +                    else None
    1.61 +
    1.62 +                  target match {
    1.63 +                    case Some((target_name, target_chunk)) =>
    1.64 +                      target_chunk.incorporate(symbol_range) match {
    1.65                          case Some(range) =>
    1.66                            val props = Position.purge(atts)
    1.67                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.68 -                          state.add_markup(false, chunk_name, info)
    1.69 +                          state.add_markup(false, target_name, info)
    1.70                          case None => bad(); state
    1.71                        }
    1.72 -                    case None => bad(); state
    1.73 +                    case None => /* FIXME bad(); */ state
    1.74                    }
    1.75  
    1.76                  case XML.Elem(Markup(name, atts), args)
    1.77 @@ -185,7 +208,7 @@
    1.78                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.79                    state.add_markup(false, Text.Chunk.Default, info)
    1.80  
    1.81 -                case _ => /* FIXME bad(); */ state
    1.82 +                case _ => bad(); state
    1.83                }
    1.84              })
    1.85          case XML.Elem(Markup(name, props), body) =>
    1.86 @@ -198,7 +221,7 @@
    1.87                if (Protocol.is_inlined(message)) {
    1.88                  for {
    1.89                    (chunk_name, chunk) <- command.chunks.iterator
    1.90 -                  range <- Protocol.message_positions(valid_id, chunk_name, chunk, message)
    1.91 +                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
    1.92                  } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
    1.93                }
    1.94                st
     2.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 16:07:02 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 19:17:28 2014 +0200
     2.3 @@ -483,11 +483,19 @@
     2.4    }
     2.5  
     2.6    final case class State private(
     2.7 +    /*reachable versions*/
     2.8      val versions: Map[Document_ID.Version, Version] = Map.empty,
     2.9 -    val blobs: Set[SHA1.Digest] = Set.empty,   // inlined files
    2.10 -    val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
    2.11 -    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
    2.12 +    /*inlined auxiliary files*/
    2.13 +    val blobs: Set[SHA1.Digest] = Set.empty,
    2.14 +    /*static markup from define_command*/
    2.15 +    val commands: Map[Document_ID.Command, Command.State] = Map.empty,
    2.16 +    /*dynamic markup from execution*/
    2.17 +    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,
    2.18 +    /*command-exec assignment for each version*/
    2.19      val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
    2.20 +    /*commands with markup produced by other commands (imm_succs)*/
    2.21 +    val augmented_commands: Graph[Document_ID.Command, Unit] = Graph.long,
    2.22 +    /*explicit (linear) history*/
    2.23      val history: History = History.init)
    2.24    {
    2.25      private def fail[A]: A = throw new State.Fail(this)
    2.26 @@ -524,23 +532,35 @@
    2.27      def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
    2.28      def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
    2.29  
    2.30 -    def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
    2.31 +    private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
    2.32        id == st.command.id ||
    2.33        (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
    2.34  
    2.35 +    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
    2.36 +      (execs.get(id) orElse commands.get(id)).map(st =>
    2.37 +        ((Text.Chunk.Id(st.command.id), st.command.chunk)))
    2.38 +
    2.39 +    private def augmented(st: Command.State): Graph[Document_ID.Command, Unit] =
    2.40 +      (augmented_commands /: st.markups.other_id_iterator)({ case (graph, id) =>
    2.41 +        graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
    2.42 +
    2.43      def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
    2.44 +    {
    2.45        execs.get(id) match {
    2.46          case Some(st) =>
    2.47 -          val new_st = st + (valid_id(st), message)
    2.48 -          (new_st, copy(execs = execs + (id -> new_st)))
    2.49 +          val new_st = st.accumulate(self_id(st), other_id _, message)
    2.50 +          val execs1 = execs + (id -> new_st)
    2.51 +          (new_st, copy(execs = execs1, augmented_commands = augmented(new_st)))
    2.52          case None =>
    2.53            commands.get(id) match {
    2.54              case Some(st) =>
    2.55 -              val new_st = st + (valid_id(st), message)
    2.56 -              (new_st, copy(commands = commands + (id -> new_st)))
    2.57 +              val new_st = st.accumulate(self_id(st), other_id _, message)
    2.58 +              val commands1 = commands + (id -> new_st)
    2.59 +              (new_st, copy(commands = commands1, augmented_commands = augmented(new_st)))
    2.60              case None => fail
    2.61            }
    2.62        }
    2.63 +    }
    2.64  
    2.65      def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
    2.66      {
    2.67 @@ -629,27 +649,48 @@
    2.68              execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
    2.69          }
    2.70        }
    2.71 -      copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
    2.72 +      copy(
    2.73 +        versions = versions1,
    2.74 +        blobs = blobs1,
    2.75 +        commands = commands1,
    2.76 +        execs = execs1,
    2.77 +        augmented_commands = augmented_commands.restrict(commands1.isDefinedAt(_)),
    2.78          assignments = assignments1)
    2.79      }
    2.80  
    2.81 -    def command_states(version: Version, command: Command): List[Command.State] =
    2.82 +    private def command_states_self(version: Version, command: Command)
    2.83 +      : List[(Document_ID.Generic, Command.State)] =
    2.84      {
    2.85        require(is_assigned(version))
    2.86        try {
    2.87          the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
    2.88 -          .map(the_dynamic_state(_)) match {
    2.89 +          .map(id => id -> the_dynamic_state(id)) match {
    2.90              case Nil => fail
    2.91 -            case states => states
    2.92 +            case res => res
    2.93            }
    2.94        }
    2.95        catch {
    2.96          case _: State.Fail =>
    2.97 -          try { List(the_static_state(command.id)) }
    2.98 -          catch { case _: State.Fail => List(command.init_state) }
    2.99 +          try { List(command.id -> the_static_state(command.id)) }
   2.100 +          catch { case _: State.Fail => List(command.id -> command.init_state) }
   2.101        }
   2.102      }
   2.103  
   2.104 +    def command_states(version: Version, command: Command): List[Command.State] =
   2.105 +    {
   2.106 +      val self = command_states_self(version, command)
   2.107 +      val others =
   2.108 +        if (augmented_commands.defined(command.id)) {
   2.109 +          (for {
   2.110 +            command_id <- augmented_commands.imm_succs(command.id).iterator
   2.111 +            (id, st) <- command_states_self(version, the_static_state(command_id).command)
   2.112 +            if !self.exists(_._1 == id)
   2.113 +          } yield (id, st)).toMap.valuesIterator.toList
   2.114 +        }
   2.115 +        else Nil
   2.116 +      self.map(_._2) ::: others.map(_.retarget(command))
   2.117 +    }
   2.118 +
   2.119      def command_results(version: Version, command: Command): Command.Results =
   2.120        Command.State.merge_results(command_states(version, command))
   2.121  
     3.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 16:07:02 2014 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 19:17:28 2014 +0200
     3.3 @@ -301,7 +301,7 @@
     3.4      Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     3.5  
     3.6    def message_positions(
     3.7 -    valid_id: Document_ID.Generic => Boolean,
     3.8 +    self_id: Document_ID.Generic => Boolean,
     3.9      chunk_name: Text.Chunk.Name,
    3.10      chunk: Text.Chunk,
    3.11      message: XML.Elem): Set[Text.Range] =
    3.12 @@ -309,7 +309,7 @@
    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, name, symbol_range)
    3.16 -        if valid_id(id) && name == chunk_name =>
    3.17 +        if self_id(id) && name == chunk_name =>
    3.18            chunk.incorporate(symbol_range) match {
    3.19              case Some(range) => set + range
    3.20              case _ => set
     4.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 08 16:07:02 2014 +0200
     4.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 08 19:17:28 2014 +0200
     4.3 @@ -106,6 +106,7 @@
     4.4    {
     4.5      sealed abstract class Name
     4.6      case object Default extends Name
     4.7 +    case class Id(id: Document_ID.Generic) extends Name
     4.8      case class File_Name(file_name: String) extends Name
     4.9  
    4.10      class File(text: CharSequence) extends Chunk