--- a/src/Pure/PIDE/document.scala Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/document.scala Sat Mar 01 12:07:26 2014 +0100
@@ -376,8 +376,32 @@
}
+ /* markup elements */
- /** global state -- document structure, execution process, editing history **/
+ 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
{
@@ -403,17 +427,21 @@
def cumulate[A](
range: Text.Range,
info: A,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]]
def select[A](
range: Text.Range,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]]
}
+
+
+ /** global state -- document structure, execution process, editing history **/
+
type Assign_Update =
List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment
@@ -672,7 +700,7 @@
def cumulate[A](
range: Text.Range,
info: A,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
@@ -708,7 +736,7 @@
def select[A](
range: Text.Range,
- elements: String => Boolean,
+ elements: Elements,
result: Command.State => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
--- a/src/Pure/PIDE/markup_tree.scala Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Sat Mar 01 12:07:26 2014 +0100
@@ -51,10 +51,10 @@
{
def markup: List[XML.Elem] = rev_markup.reverse
- def filter_markup(pred: String => Boolean): List[XML.Elem] =
+ def filter_markup(elements: Document.Elements): List[XML.Elem] =
{
var result: List[XML.Elem] = Nil
- for { elem <- rev_markup; if (pred(elem.name)) }
+ for { elem <- rev_markup; if (elements(elem.name)) }
result ::= elem
result.toList
}
@@ -194,7 +194,7 @@
def to_XML(text: CharSequence): XML.Body =
to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
- def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
+ def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
def results(x: A, entry: Entry): Option[A] =
--- a/src/Pure/PIDE/protocol.scala Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Sat Mar 01 12:07:26 2014 +0100
@@ -77,11 +77,11 @@
def command_status(markups: List[Markup]): Status =
(Status.init /: markups)(command_status(_, _))
- val command_status_elements: Set[String] =
- Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+ val command_status_elements =
+ Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
Markup.FINISHED, Markup.FAILED)
- val status_elements: Set[String] =
+ val status_elements =
command_status_elements + Markup.WARNING + Markup.ERROR
@@ -165,7 +165,8 @@
/* result messages */
- private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
+ private val clean_elements =
+ Document.Elements(Markup.REPORT, Markup.NO_REPORT)
def clean_message(body: XML.Body): XML.Body =
body filter {
@@ -276,7 +277,7 @@
/* reported positions */
private val position_elements =
- Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+ Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(
command_id: Document_ID.Command,
--- a/src/Tools/jEdit/src/rendering.scala Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 01 12:07:26 2014 +0100
@@ -150,28 +150,29 @@
/* markup elements */
- private val completion_names_elements = Set(Markup.COMPLETION)
+ private val completion_names_elements =
+ Document.Elements(Markup.COMPLETION)
private val language_context_elements =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
private val highlight_elements =
- Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Document.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 =
- Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+ Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
private val active_elements =
- Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+ Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
Markup.SENDBACK, Markup.SIMP_TRACE)
private val tooltip_message_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+ Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
private val tooltip_descriptions =
Map(
@@ -184,22 +185,23 @@
Markup.TVAR -> "schematic type variable")
private val tooltip_elements =
- Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+ Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
- tooltip_descriptions.keys
+ Document.Elements(tooltip_descriptions.keySet)
private val gutter_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
private val squiggly_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
private val line_background_elements =
- Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+ Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
Markup.INFORMATION)
- private val separator_elements = Set(Markup.SEPARATOR)
+ private val separator_elements =
+ Document.Elements(Markup.SEPARATOR)
private val background_elements =
Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
@@ -208,13 +210,14 @@
active_elements
private val foreground_elements =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.ANTIQUOTED)
- private val bullet_elements = Set(Markup.BULLET)
+ private val bullet_elements =
+ Document.Elements(Markup.BULLET)
private val fold_depth_elements =
- Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+ Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
}
@@ -421,7 +424,7 @@
def command_results(range: Text.Range): Command.Results =
{
val results =
- snapshot.select[Command.Results](range, _ => true, command_state =>
+ snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
{ case _ => Some(command_state.results) }).map(_.info)
(Command.Results.empty /: results)(_ ++ _)
}
@@ -703,7 +706,8 @@
Markup.ML_STRING -> inner_quoted_color,
Markup.ML_COMMENT -> inner_comment_color)
- private lazy val text_color_elements = text_colors.keySet
+ private lazy val text_color_elements =
+ Document.Elements(text_colors.keySet)
def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
{