--- 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)
}
--- 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]] =
{
--- 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 =
--- 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"
--- 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
--- 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,
--- 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
--- 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]] =
{