--- a/src/Pure/PIDE/command.scala Fri Feb 21 13:36:40 2014 +0100
+++ b/src/Pure/PIDE/command.scala Fri Feb 21 15:12:50 2014 +0100
@@ -56,18 +56,59 @@
}
+ /* markup */
+
+ object Markup_Index
+ {
+ val markup: Markup_Index = Markup_Index(false, "")
+ }
+
+ sealed case class Markup_Index(status: Boolean, file_name: String)
+
+ object Markups
+ {
+ val empty: Markups = new Markups(Map.empty)
+
+ def init(markup: Markup_Tree): Markups =
+ new Markups(Map(Markup_Index.markup -> markup))
+ }
+
+ final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
+ {
+ def apply(index: Markup_Index): Markup_Tree =
+ rep.getOrElse(index, Markup_Tree.empty)
+
+ def add(index: Markup_Index, markup: Text.Markup): Markups =
+ new Markups(rep + (index -> (this(index) + markup)))
+
+ def ++ (other: Markups): Markups =
+ new Markups(
+ (rep.keySet ++ other.rep.keySet)
+ .map(index => index -> (this(index) ++ other(index))).toMap)
+
+ override def hashCode: Int = rep.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Markups => rep == other.rep
+ case _ => false
+ }
+ override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
+ }
+
+
/* state */
sealed case class State(
command: Command,
status: List[Markup] = Nil,
results: Results = Results.empty,
- markups: Map[String, Markup_Tree] = Map.empty)
+ markups: Markups = Markups.empty)
{
- def get_markup(file_name: String): Markup_Tree =
- markups.getOrElse(file_name, Markup_Tree.empty)
+ /* markup */
- def markup: Markup_Tree = get_markup("")
+ def get_markup(index: Markup_Index): Markup_Tree = markups(index)
+
+ def markup: Markup_Tree = get_markup(Markup_Index.markup)
def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
markup.to_XML(command.range, command.source, filter)
@@ -81,10 +122,17 @@
results == other.results &&
markups == other.markups
- private def add_status(st: Markup): State = copy(status = st :: status)
+ private def add_status(st: Markup): State =
+ copy(status = st :: status)
- private def add_markup(file_name: String, m: Text.Markup): State =
- copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
+ private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
+ {
+ val markups1 =
+ if (status || Protocol.status_elements(m.info.name))
+ markups.add(Markup_Index(true, file_name), m)
+ else markups
+ copy(markups = markups1.add(Markup_Index(false, file_name), m))
+ }
def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
message match {
@@ -92,8 +140,9 @@
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
- state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
-
+ state.
+ add_status(markup).
+ add_markup(true, "", Text.Info(command.proper_range, elem))
case _ =>
System.err.println("Ignored status message: " + msg)
state
@@ -113,8 +162,8 @@
case Some(range) =>
if (!range.is_singularity) {
val props = Position.purge(atts)
- state.add_markup(file_name,
- Text.Info(range, XML.Elem(Markup(name, props), args)))
+ val info = Text.Info(range, XML.Elem(Markup(name, props), args))
+ state.add_markup(false, file_name, info)
}
else state
case None => bad(); state
@@ -127,7 +176,7 @@
val range = command.proper_range
val props = Position.purge(atts)
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup("", info)
+ state.add_markup(false, "", info)
case _ => /* FIXME bad(); */ state
}
@@ -143,7 +192,7 @@
for {
(file_name, chunk) <- command.chunks
range <- Protocol.message_positions(command.id, alt_id, chunk, message)
- } st = st.add_markup(file_name, Text.Info(range, message2))
+ } st = st.add_markup(false, file_name, Text.Info(range, message2))
}
st
@@ -157,9 +206,7 @@
copy(
status = other.status ::: status,
results = results ++ other.results,
- markups =
- (markups.keySet ++ other.markups.keySet)
- .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
+ markups = markups ++ other.markups
)
}
@@ -324,7 +371,7 @@
/* accumulated results */
val init_state: Command.State =
- Command.State(this, results = init_results, markups = Map("" -> init_markup))
+ Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
val empty_state: Command.State = Command.State(this)
}