# HG changeset patch
# User wenzelm
# Date 1398510440 -7200
# Node ID 81370dfadb1d05f9c9f0415fb7417dbeee459730
# Parent  e4f363e16bdc84f1f84b50867cef730a6765d609
tuned signature;

diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -115,7 +115,7 @@
       Results.merge(states.map(_.results))
 
     def merge_markup(states: List[State], index: Markup_Index,
-        range: Text.Range, elements: Document.Elements): Markup_Tree =
+        range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Markup_Tree.merge(states.map(_.markup(index)), range, elements)
   }
 
diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -379,31 +379,6 @@
   }
 
 
-  /* markup elements */
-
-  object Elements
-  {
-    def apply(elems: Set[String]): Elements = new Elements(elems)
-    def apply(elems: String*): Elements = apply(Set(elems: _*))
-    val empty: Elements = apply()
-    val full: Elements = new Full_Elements
-  }
-
-  sealed class Elements private[Document](private val rep: Set[String])
-  {
-    def apply(elem: String): Boolean = rep.contains(elem)
-    def + (elem: String): Elements = new Elements(rep + elem)
-    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
-    override def toString: String = rep.mkString("Elements(", ",", ")")
-  }
-
-  private class Full_Elements extends Elements(Set.empty)
-  {
-    override def apply(elem: String): Boolean = true
-    override def toString: String = "Full_Elements()"
-  }
-
-
   /* snapshot */
 
   object Snapshot
@@ -431,13 +406,13 @@
     def cumulate[A](
       range: Text.Range,
       info: A,
-      elements: Elements,
+      elements: Markup.Elements,
       result: List[Command.State] => (A, Text.Markup) => Option[A],
       status: Boolean = false): List[Text.Info[A]]
 
     def select[A](
       range: Text.Range,
-      elements: Elements,
+      elements: Markup.Elements,
       result: List[Command.State] => Text.Markup => Option[A],
       status: Boolean = false): List[Text.Info[A]]
   }
@@ -697,10 +672,10 @@
       Command.State.merge_results(command_states(version, command))
 
     def command_markup(version: Version, command: Command, index: Command.Markup_Index,
-        range: Text.Range, elements: Elements): Markup_Tree =
+        range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Command.State.merge_markup(command_states(version, command), index, range, elements)
 
-    def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
+    def markup_to_XML(version: Version, node: Node, elements: Markup.Elements): XML.Body =
       (for {
         command <- node.commands.iterator
         markup =
@@ -769,7 +744,7 @@
         def cumulate[A](
           range: Text.Range,
           info: A,
-          elements: Elements,
+          elements: Markup.Elements,
           result: List[Command.State] => (A, Text.Markup) => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
@@ -797,7 +772,7 @@
 
         def select[A](
           range: Text.Range,
-          elements: Elements,
+          elements: Markup.Elements,
           result: List[Command.State] => Text.Markup => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Apr 26 13:07:20 2014 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/PIDE/markup.ML
     Author:     Makarius
 
-Isabelle-specific implementation of quasi-abstract markup elements.
+Quasi-abstract markup elements.
 *)
 
 signature MARKUP =
diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -2,7 +2,7 @@
     Module:     PIDE
     Author:     Makarius
 
-Isabelle-specific implementation of quasi-abstract markup elements.
+Quasi-abstract markup elements.
 */
 
 package isabelle
@@ -10,6 +10,30 @@
 
 object Markup
 {
+  /* elements */
+
+  object Elements
+  {
+    def apply(elems: Set[String]): Elements = new Elements(elems)
+    def apply(elems: String*): Elements = apply(Set(elems: _*))
+    val empty: Elements = apply()
+    val full: Elements =
+      new Elements(Set.empty)
+      {
+        override def apply(elem: String): Boolean = true
+        override def toString: String = "Elements.full"
+      }
+  }
+
+  sealed class Elements private[Markup](private val rep: Set[String])
+  {
+    def apply(elem: String): Boolean = rep.contains(elem)
+    def + (elem: String): Elements = new Elements(rep + elem)
+    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
+    override def toString: String = rep.mkString("Elements(", ",", ")")
+  }
+
+
   /* properties */
 
   val NAME = "name"
diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -20,7 +20,7 @@
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
-  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
+  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
     (empty /: trees)(_.merge(_, range, elements))
 
   def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
@@ -54,7 +54,7 @@
   {
     def markup: List[XML.Elem] = rev_markup.reverse
 
-    def filter_markup(elements: Document.Elements): List[XML.Elem] =
+    def filter_markup(elements: Markup.Elements): List[XML.Elem] =
     {
       var result: List[XML.Elem] = Nil
       for { elem <- rev_markup; if (elements(elem.name)) }
@@ -161,7 +161,7 @@
     }
   }
 
-  def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
+  def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
   {
     def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
       (tree1 /: tree2.branches)(
@@ -181,7 +181,7 @@
     }
   }
 
-  def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
+  def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
     result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   {
     def results(x: A, entry: Entry): Option[A] =
@@ -230,7 +230,7 @@
       List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
   }
 
-  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
+  def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
   {
     def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
       if (start == stop) Nil
diff -r e4f363e16bdc -r 81370dfadb1d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -101,7 +101,7 @@
   }
 
   val proper_status_elements =
-    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       Markup.FINISHED, Markup.FAILED)
 
   val liberal_status_elements =
@@ -187,7 +187,7 @@
   /* result messages */
 
   private val clean_elements =
-    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
+    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_message(body: XML.Body): XML.Body =
     body filter {
@@ -308,7 +308,7 @@
   /* reported positions */
 
   private val position_elements =
-    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
     self_id: Document_ID.Generic => Boolean,
diff -r e4f363e16bdc -r 81370dfadb1d src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -162,7 +162,7 @@
           val markup =
             snapshot.state.command_markup(
               snapshot.version, command, Command.Markup_Index.markup,
-                command.range, Document.Elements.full)
+                command.range, Markup.Elements.full)
           Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
               {
                 val range = info.range + command_start
diff -r e4f363e16bdc -r 81370dfadb1d src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -129,28 +129,28 @@
   /* markup elements */
 
   private val semantic_completion_elements =
-    Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
+    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
 
   private val language_context_elements =
-    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+    Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)
 
   private val highlight_elements =
-    Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+    Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
       Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR)
 
   private val hyperlink_elements =
-    Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
 
   private val active_elements =
-    Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
       Markup.SENDBACK, Markup.SIMP_TRACE)
 
   private val tooltip_message_elements =
-    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
 
   private val tooltip_descriptions =
     Map(
@@ -163,23 +163,23 @@
       Markup.TVAR -> "schematic type variable")
 
   private val tooltip_elements =
-    Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+    Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
       Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
-    Document.Elements(tooltip_descriptions.keySet)
+    Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
-    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   private val squiggly_elements =
-    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   private val line_background_elements =
-    Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
       Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
       Markup.INFORMATION)
 
   private val separator_elements =
-    Document.Elements(Markup.SEPARATOR)
+    Markup.Elements(Markup.SEPARATOR)
 
   private val background_elements =
     Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
@@ -188,14 +188,14 @@
       active_elements
 
   private val foreground_elements =
-    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+    Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.ANTIQUOTED)
 
   private val bullet_elements =
-    Document.Elements(Markup.BULLET)
+    Markup.Elements(Markup.BULLET)
 
   private val fold_depth_elements =
-    Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+    Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 }
 
 
@@ -287,7 +287,7 @@
   /* spell checker */
 
   private lazy val spell_checker_elements =
-    Document.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
+    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
 
   def spell_checker_ranges(range: Text.Range): List[Text.Range] =
     snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
@@ -407,7 +407,7 @@
 
   def command_results(range: Text.Range): Command.Results =
     Command.State.merge_results(
-      snapshot.select[List[Command.State]](range, Document.Elements.full, command_states =>
+      snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
         { case _ => Some(command_states) }).flatMap(_.info))
 
 
@@ -695,7 +695,7 @@
       Markup.SML_COMMENT -> inner_comment_color)
 
   private lazy val text_color_elements =
-    Document.Elements(text_colors.keySet)
+    Markup.Elements(text_colors.keySet)
 
   def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   {