--- a/src/Pure/PIDE/command.scala Sun Mar 15 23:46:00 2015 +0100
+++ b/src/Pure/PIDE/command.scala Mon Mar 16 11:07:56 2015 +0100
@@ -234,7 +234,7 @@
if (Protocol.is_inlined(message)) {
for {
(chunk_name, chunk) <- command.chunks.iterator
- range <- Protocol.message_positions(
+ range <- Protocol_Message.positions(
self_id, command.position, chunk_name, chunk, message)
} st = st.add_markup(false, chunk_name, Text.Info(range, message2))
}
--- a/src/Pure/PIDE/protocol.scala Sun Mar 15 23:46:00 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Mar 16 11:07:56 2015 +0100
@@ -186,34 +186,6 @@
/* result messages */
- private val clean_elements =
- Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
-
- def clean_message(body: XML.Body): XML.Body =
- body filter {
- case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
- case XML.Elem(Markup(name, _), _) => !clean_elements(name)
- case _ => true
- } map {
- case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
- case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
- case t => t
- }
-
- def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
- body flatMap {
- case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
- List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
- case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
- List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
- case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
- case XML.Elem(_, ts) => message_reports(props, ts)
- case XML.Text(_) => Nil
- }
-
-
- /* specific messages */
-
def is_result(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -302,53 +274,6 @@
case _ => None
}
}
-
-
- /* reported positions */
-
- private val position_elements =
- Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-
- def message_positions(
- self_id: Document_ID.Generic => Boolean,
- command_position: Position.T,
- chunk_name: Symbol.Text_Chunk.Name,
- chunk: Symbol.Text_Chunk,
- message: XML.Elem): Set[Text.Range] =
- {
- def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
- props match {
- case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
- val opt_range =
- Position.Range.unapply(props) orElse {
- if (name == Symbol.Text_Chunk.Default)
- Position.Range.unapply(command_position)
- else None
- }
- opt_range match {
- case Some(symbol_range) =>
- chunk.incorporate(symbol_range) match {
- case Some(range) => set + range
- case _ => set
- }
- case None => set
- }
- case _ => set
- }
-
- def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
- tree match {
- case XML.Wrapped_Elem(Markup(name, props), _, body) =>
- body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
- case XML.Elem(Markup(name, props), body) =>
- body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
- case XML.Text(_) => set
- }
-
- val set = positions(Set.empty, message)
- if (set.isEmpty) elem_positions(message.markup.properties, set)
- else set
- }
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_message.scala Mon Mar 16 11:07:56 2015 +0100
@@ -0,0 +1,84 @@
+/* Title: Pure/PIDE/protocol_message.scala
+ Author: Makarius
+
+Auxiliary operations on protocol messages.
+*/
+
+package isabelle
+
+
+object Protocol_Message
+{
+ /* inlined reports */
+
+ private val report_elements =
+ Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
+
+ def clean_reports(body: XML.Body): XML.Body =
+ body filter {
+ case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
+ case XML.Elem(Markup(name, _), _) => !report_elements(name)
+ case _ => true
+ } map {
+ case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
+ case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
+ case t => t
+ }
+
+ def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
+ body flatMap {
+ case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
+ List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
+ case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
+ List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
+ case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
+ case XML.Elem(_, ts) => reports(props, ts)
+ case XML.Text(_) => Nil
+ }
+
+
+ /* reported positions */
+
+ private val position_elements =
+ Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
+ def positions(
+ self_id: Document_ID.Generic => Boolean,
+ command_position: Position.T,
+ chunk_name: Symbol.Text_Chunk.Name,
+ chunk: Symbol.Text_Chunk,
+ message: XML.Elem): Set[Text.Range] =
+ {
+ def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
+ props match {
+ case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
+ val opt_range =
+ Position.Range.unapply(props) orElse {
+ if (name == Symbol.Text_Chunk.Default)
+ Position.Range.unapply(command_position)
+ else None
+ }
+ opt_range match {
+ case Some(symbol_range) =>
+ chunk.incorporate(symbol_range) match {
+ case Some(range) => set + range
+ case _ => set
+ }
+ case None => set
+ }
+ case _ => set
+ }
+ def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
+ t match {
+ case XML.Wrapped_Elem(Markup(name, props), _, body) =>
+ body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
+ case XML.Elem(Markup(name, props), body) =>
+ body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
+ case XML.Text(_) => set
+ }
+
+ val set = tree(Set.empty, message)
+ if (set.isEmpty) elem(message.markup.properties, set)
+ else set
+ }
+}
--- a/src/Pure/PIDE/prover.scala Sun Mar 15 23:46:00 2015 +0100
+++ b/src/Pure/PIDE/prover.scala Mon Mar 16 11:07:56 2015 +0100
@@ -108,8 +108,8 @@
{
if (kind == Markup.INIT) system_channel.accepted()
- val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
- val reports = Protocol.message_reports(props, body)
+ val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
+ val reports = Protocol_Message.reports(props, body)
for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
}
--- a/src/Pure/build-jars Sun Mar 15 23:46:00 2015 +0100
+++ b/src/Pure/build-jars Mon Mar 16 11:07:56 2015 +0100
@@ -64,6 +64,7 @@
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
+ PIDE/protocol_message.scala
PIDE/prover.scala
PIDE/query_operation.scala
PIDE/resources.scala