more general / abstract Command.Markups, with separate index for status elements;
slightly faster Rendering.overview_color;
--- 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)
}--- a/src/Pure/PIDE/document.scala Fri Feb 21 13:36:40 2014 +0100
+++ b/src/Pure/PIDE/document.scala Fri Feb 21 15:12:50 2014 +0100
@@ -357,6 +357,7 @@
val state: State
val version: Version
val is_outdated: Boolean
+
def convert(i: Text.Offset): Text.Offset
def revert(i: Text.Offset): Text.Offset
def convert(range: Text.Range): Text.Range
@@ -366,6 +367,16 @@
val node: Node
val thy_load_commands: List[Command]
def eq_content(other: Snapshot): Boolean
+
+ def cumulate_status[A](
+ range: Text.Range,
+ info: A,
+ elements: String => Boolean,
+ result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
+ def select_status[A](
+ range: Text.Range,
+ elements: String => Boolean,
+ result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
def cumulate_markup[A](
range: Text.Range,
info: A,
@@ -601,14 +612,14 @@
val version = stable.version.get_finished
val is_outdated = !(pending_edits.isEmpty && latest == stable)
+
+ /* local node content */
+
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
-
- /* local node content */
-
val node_name = name
val node = version.nodes(name)
@@ -629,37 +640,47 @@
(thy_load_commands zip other.thy_load_commands).forall(eq_commands)
}
- def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
+
+ /* cumulate markup */
+
+ private def cumulate[A](
+ status: Boolean,
+ range: Text.Range,
+ info: A,
+ elements: String => Boolean,
result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
val former_range = revert(range)
thy_load_commands match {
case thy_load_command :: _ =>
val file_name = node_name.node
+ val markup_index = Command.Markup_Index(status, file_name)
(for {
chunk <- thy_load_command.chunks.get(file_name).iterator
st = state.command_state(version, thy_load_command)
res = result(st)
- Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
+ Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
former_range.restrict(chunk.range), info, elements,
{ case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
).iterator
} yield Text.Info(convert(r0), a)).toList
case _ =>
+ val markup_index = Command.Markup_Index(status, "")
(for {
(command, command_start) <- node.command_range(former_range)
st = state.command_state(version, command)
res = result(st)
- Text.Info(r0, a) <- st.markup.cumulate[A](
+ Text.Info(r0, a) <- st.get_markup(markup_index).cumulate[A](
(former_range - command_start).restrict(command.range), info, elements,
- { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
- ).iterator
+ {
+ case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
+ }).iterator
} yield Text.Info(convert(r0 + command_start), a)).toList
}
}
- def select_markup[A](range: Text.Range, elements: String => Boolean,
+ private def select[A](status: Boolean, range: Text.Range, elements: String => Boolean,
result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
{
def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
@@ -674,6 +695,22 @@
for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
yield Text.Info(r, x)
}
+
+ def cumulate_status[A](range: Text.Range, info: A, elements: String => Boolean,
+ result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
+ cumulate(true, range, info, elements, result)
+
+ def select_status[A](range: Text.Range, elements: String => Boolean,
+ result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
+ select(true, range, elements, result)
+
+ def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
+ result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
+ cumulate(false, range, info, elements, result)
+
+ def select_markup[A](range: Text.Range, elements: String => Boolean,
+ result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
+ select(false, range, elements, result)
}
}
}--- a/src/Tools/jEdit/src/rendering.scala Fri Feb 21 13:36:40 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Fri Feb 21 15:12:50 2014 +0100
@@ -301,7 +301,7 @@
if (snapshot.is_outdated) None
else {
val results =
- snapshot.cumulate_markup[(Protocol.Status, Int)](
+ snapshot.cumulate_status[(Protocol.Status, Int)](
range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
{
case ((status, pri), Text.Info(_, elem)) =>