tuned signature -- more explicit Document.Elements;
authorwenzelm
Sat Mar 01 12:07:26 2014 +0100 (2014-03-01)
changeset 5582061869776ce1f
parent 55817 0bc0217387a5
child 55821 44055f07cbd8
tuned signature -- more explicit Document.Elements;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 01 09:34:08 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 01 12:07:26 2014 +0100
     1.3 @@ -376,8 +376,32 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* markup elements */
     1.8  
     1.9 -  /** global state -- document structure, execution process, editing history **/
    1.10 +  object Elements
    1.11 +  {
    1.12 +    def apply(elems: Set[String]): Elements = new Elements(elems)
    1.13 +    def apply(elems: String*): Elements = apply(Set(elems: _*))
    1.14 +    val empty: Elements = apply()
    1.15 +    val full: Elements = new Full_Elements
    1.16 +  }
    1.17 +
    1.18 +  sealed class Elements private[Document](private val rep: Set[String])
    1.19 +  {
    1.20 +    def apply(elem: String): Boolean = rep.contains(elem)
    1.21 +    def + (elem: String): Elements = new Elements(rep + elem)
    1.22 +    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
    1.23 +    override def toString: String = rep.mkString("Elements(", ",", ")")
    1.24 +  }
    1.25 +
    1.26 +  private class Full_Elements extends Elements(Set.empty)
    1.27 +  {
    1.28 +    override def apply(elem: String): Boolean = true
    1.29 +    override def toString: String = "Full_Elements()"
    1.30 +  }
    1.31 +
    1.32 +
    1.33 +  /* snapshot */
    1.34  
    1.35    object Snapshot
    1.36    {
    1.37 @@ -403,17 +427,21 @@
    1.38      def cumulate[A](
    1.39        range: Text.Range,
    1.40        info: A,
    1.41 -      elements: String => Boolean,
    1.42 +      elements: Elements,
    1.43        result: Command.State => (A, Text.Markup) => Option[A],
    1.44        status: Boolean = false): List[Text.Info[A]]
    1.45  
    1.46      def select[A](
    1.47        range: Text.Range,
    1.48 -      elements: String => Boolean,
    1.49 +      elements: Elements,
    1.50        result: Command.State => Text.Markup => Option[A],
    1.51        status: Boolean = false): List[Text.Info[A]]
    1.52    }
    1.53  
    1.54 +
    1.55 +
    1.56 +  /** global state -- document structure, execution process, editing history **/
    1.57 +
    1.58    type Assign_Update =
    1.59      List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
    1.60  
    1.61 @@ -672,7 +700,7 @@
    1.62          def cumulate[A](
    1.63            range: Text.Range,
    1.64            info: A,
    1.65 -          elements: String => Boolean,
    1.66 +          elements: Elements,
    1.67            result: Command.State => (A, Text.Markup) => Option[A],
    1.68            status: Boolean = false): List[Text.Info[A]] =
    1.69          {
    1.70 @@ -708,7 +736,7 @@
    1.71  
    1.72          def select[A](
    1.73            range: Text.Range,
    1.74 -          elements: String => Boolean,
    1.75 +          elements: Elements,
    1.76            result: Command.State => Text.Markup => Option[A],
    1.77            status: Boolean = false): List[Text.Info[A]] =
    1.78          {
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Mar 01 09:34:08 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Mar 01 12:07:26 2014 +0100
     2.3 @@ -51,10 +51,10 @@
     2.4    {
     2.5      def markup: List[XML.Elem] = rev_markup.reverse
     2.6  
     2.7 -    def filter_markup(pred: String => Boolean): List[XML.Elem] =
     2.8 +    def filter_markup(elements: Document.Elements): List[XML.Elem] =
     2.9      {
    2.10        var result: List[XML.Elem] = Nil
    2.11 -      for { elem <- rev_markup; if (pred(elem.name)) }
    2.12 +      for { elem <- rev_markup; if (elements(elem.name)) }
    2.13          result ::= elem
    2.14        result.toList
    2.15      }
    2.16 @@ -194,7 +194,7 @@
    2.17    def to_XML(text: CharSequence): XML.Body =
    2.18      to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
    2.19  
    2.20 -  def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
    2.21 +  def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
    2.22      result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    2.23    {
    2.24      def results(x: A, entry: Entry): Option[A] =
     3.1 --- a/src/Pure/PIDE/protocol.scala	Sat Mar 01 09:34:08 2014 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Mar 01 12:07:26 2014 +0100
     3.3 @@ -77,11 +77,11 @@
     3.4    def command_status(markups: List[Markup]): Status =
     3.5      (Status.init /: markups)(command_status(_, _))
     3.6  
     3.7 -  val command_status_elements: Set[String] =
     3.8 -    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     3.9 +  val command_status_elements =
    3.10 +    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    3.11        Markup.FINISHED, Markup.FAILED)
    3.12  
    3.13 -  val status_elements: Set[String] =
    3.14 +  val status_elements =
    3.15      command_status_elements + Markup.WARNING + Markup.ERROR
    3.16  
    3.17  
    3.18 @@ -165,7 +165,8 @@
    3.19  
    3.20    /* result messages */
    3.21  
    3.22 -  private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
    3.23 +  private val clean_elements =
    3.24 +    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
    3.25  
    3.26    def clean_message(body: XML.Body): XML.Body =
    3.27      body filter {
    3.28 @@ -276,7 +277,7 @@
    3.29    /* reported positions */
    3.30  
    3.31    private val position_elements =
    3.32 -    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    3.33 +    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    3.34  
    3.35    def message_positions(
    3.36      command_id: Document_ID.Command,
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 09:34:08 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 12:07:26 2014 +0100
     4.3 @@ -150,28 +150,29 @@
     4.4  
     4.5    /* markup elements */
     4.6  
     4.7 -  private val completion_names_elements = Set(Markup.COMPLETION)
     4.8 +  private val completion_names_elements =
     4.9 +    Document.Elements(Markup.COMPLETION)
    4.10  
    4.11    private val language_context_elements =
    4.12 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    4.13 +    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    4.14        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
    4.15        Markup.ML_STRING, Markup.ML_COMMENT)
    4.16  
    4.17    private val highlight_elements =
    4.18 -    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    4.19 +    Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    4.20        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    4.21        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    4.22        Markup.VAR, Markup.TFREE, Markup.TVAR)
    4.23  
    4.24    private val hyperlink_elements =
    4.25 -    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    4.26 +    Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    4.27  
    4.28    private val active_elements =
    4.29 -    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    4.30 +    Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    4.31        Markup.SENDBACK, Markup.SIMP_TRACE)
    4.32  
    4.33    private val tooltip_message_elements =
    4.34 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    4.35 +    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    4.36  
    4.37    private val tooltip_descriptions =
    4.38      Map(
    4.39 @@ -184,22 +185,23 @@
    4.40        Markup.TVAR -> "schematic type variable")
    4.41  
    4.42    private val tooltip_elements =
    4.43 -    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    4.44 +    Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    4.45        Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    4.46 -      tooltip_descriptions.keys
    4.47 +    Document.Elements(tooltip_descriptions.keySet)
    4.48  
    4.49    private val gutter_elements =
    4.50 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    4.51 +    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    4.52  
    4.53    private val squiggly_elements =
    4.54 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    4.55 +    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    4.56  
    4.57    private val line_background_elements =
    4.58 -    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    4.59 +    Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    4.60        Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
    4.61        Markup.INFORMATION)
    4.62  
    4.63 -  private val separator_elements = Set(Markup.SEPARATOR)
    4.64 +  private val separator_elements =
    4.65 +    Document.Elements(Markup.SEPARATOR)
    4.66  
    4.67    private val background_elements =
    4.68      Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
    4.69 @@ -208,13 +210,14 @@
    4.70        active_elements
    4.71  
    4.72    private val foreground_elements =
    4.73 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    4.74 +    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    4.75        Markup.CARTOUCHE, Markup.ANTIQUOTED)
    4.76  
    4.77 -  private val bullet_elements = Set(Markup.BULLET)
    4.78 +  private val bullet_elements =
    4.79 +    Document.Elements(Markup.BULLET)
    4.80  
    4.81    private val fold_depth_elements =
    4.82 -    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    4.83 +    Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    4.84  }
    4.85  
    4.86  
    4.87 @@ -421,7 +424,7 @@
    4.88    def command_results(range: Text.Range): Command.Results =
    4.89    {
    4.90      val results =
    4.91 -      snapshot.select[Command.Results](range, _ => true, command_state =>
    4.92 +      snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
    4.93          { case _ => Some(command_state.results) }).map(_.info)
    4.94      (Command.Results.empty /: results)(_ ++ _)
    4.95    }
    4.96 @@ -703,7 +706,8 @@
    4.97        Markup.ML_STRING -> inner_quoted_color,
    4.98        Markup.ML_COMMENT -> inner_comment_color)
    4.99  
   4.100 -  private lazy val text_color_elements = text_colors.keySet
   4.101 +  private lazy val text_color_elements =
   4.102 +    Document.Elements(text_colors.keySet)
   4.103  
   4.104    def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   4.105    {