# HG changeset patch
# User wenzelm
# Date 1426500476 -3600
# Node ID 6da3efec20ca244268286559f65b57cd056a806c
# Parent  5b0003211207747af7eae48ada7e0fddb4c18960
clarified modules;

diff -r 5b0003211207 -r 6da3efec20ca src/Pure/PIDE/command.scala
--- 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))
               }
diff -r 5b0003211207 -r 6da3efec20ca src/Pure/PIDE/protocol.scala
--- 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
-  }
 }
 
 
diff -r 5b0003211207 -r 6da3efec20ca src/Pure/PIDE/protocol_message.scala
--- /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
+  }
+}
diff -r 5b0003211207 -r 6da3efec20ca src/Pure/PIDE/prover.scala
--- 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)))
   }
 
diff -r 5b0003211207 -r 6da3efec20ca src/Pure/build-jars
--- 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