tuned signature;
authorwenzelm
Sat Apr 26 13:07:20 2014 +0200 (2014-04-26 ago)
changeset 5674381370dfadb1d
parent 56737 e4f363e16bdc
child 56744 0b74d1df4b8e
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Apr 26 06:43:06 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Apr 26 13:07:20 2014 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4        Results.merge(states.map(_.results))
     1.5  
     1.6      def merge_markup(states: List[State], index: Markup_Index,
     1.7 -        range: Text.Range, elements: Document.Elements): Markup_Tree =
     1.8 +        range: Text.Range, elements: Markup.Elements): Markup_Tree =
     1.9        Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    1.10    }
    1.11  
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 26 06:43:06 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 26 13:07:20 2014 +0200
     2.3 @@ -379,31 +379,6 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* markup elements */
     2.8 -
     2.9 -  object Elements
    2.10 -  {
    2.11 -    def apply(elems: Set[String]): Elements = new Elements(elems)
    2.12 -    def apply(elems: String*): Elements = apply(Set(elems: _*))
    2.13 -    val empty: Elements = apply()
    2.14 -    val full: Elements = new Full_Elements
    2.15 -  }
    2.16 -
    2.17 -  sealed class Elements private[Document](private val rep: Set[String])
    2.18 -  {
    2.19 -    def apply(elem: String): Boolean = rep.contains(elem)
    2.20 -    def + (elem: String): Elements = new Elements(rep + elem)
    2.21 -    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
    2.22 -    override def toString: String = rep.mkString("Elements(", ",", ")")
    2.23 -  }
    2.24 -
    2.25 -  private class Full_Elements extends Elements(Set.empty)
    2.26 -  {
    2.27 -    override def apply(elem: String): Boolean = true
    2.28 -    override def toString: String = "Full_Elements()"
    2.29 -  }
    2.30 -
    2.31 -
    2.32    /* snapshot */
    2.33  
    2.34    object Snapshot
    2.35 @@ -431,13 +406,13 @@
    2.36      def cumulate[A](
    2.37        range: Text.Range,
    2.38        info: A,
    2.39 -      elements: Elements,
    2.40 +      elements: Markup.Elements,
    2.41        result: List[Command.State] => (A, Text.Markup) => Option[A],
    2.42        status: Boolean = false): List[Text.Info[A]]
    2.43  
    2.44      def select[A](
    2.45        range: Text.Range,
    2.46 -      elements: Elements,
    2.47 +      elements: Markup.Elements,
    2.48        result: List[Command.State] => Text.Markup => Option[A],
    2.49        status: Boolean = false): List[Text.Info[A]]
    2.50    }
    2.51 @@ -697,10 +672,10 @@
    2.52        Command.State.merge_results(command_states(version, command))
    2.53  
    2.54      def command_markup(version: Version, command: Command, index: Command.Markup_Index,
    2.55 -        range: Text.Range, elements: Elements): Markup_Tree =
    2.56 +        range: Text.Range, elements: Markup.Elements): Markup_Tree =
    2.57        Command.State.merge_markup(command_states(version, command), index, range, elements)
    2.58  
    2.59 -    def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
    2.60 +    def markup_to_XML(version: Version, node: Node, elements: Markup.Elements): XML.Body =
    2.61        (for {
    2.62          command <- node.commands.iterator
    2.63          markup =
    2.64 @@ -769,7 +744,7 @@
    2.65          def cumulate[A](
    2.66            range: Text.Range,
    2.67            info: A,
    2.68 -          elements: Elements,
    2.69 +          elements: Markup.Elements,
    2.70            result: List[Command.State] => (A, Text.Markup) => Option[A],
    2.71            status: Boolean = false): List[Text.Info[A]] =
    2.72          {
    2.73 @@ -797,7 +772,7 @@
    2.74  
    2.75          def select[A](
    2.76            range: Text.Range,
    2.77 -          elements: Elements,
    2.78 +          elements: Markup.Elements,
    2.79            result: List[Command.State] => Text.Markup => Option[A],
    2.80            status: Boolean = false): List[Text.Info[A]] =
    2.81          {
     3.1 --- a/src/Pure/PIDE/markup.ML	Sat Apr 26 06:43:06 2014 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Sat Apr 26 13:07:20 2014 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      Pure/PIDE/markup.ML
     3.5      Author:     Makarius
     3.6  
     3.7 -Isabelle-specific implementation of quasi-abstract markup elements.
     3.8 +Quasi-abstract markup elements.
     3.9  *)
    3.10  
    3.11  signature MARKUP =
     4.1 --- a/src/Pure/PIDE/markup.scala	Sat Apr 26 06:43:06 2014 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 26 13:07:20 2014 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4      Module:     PIDE
     4.5      Author:     Makarius
     4.6  
     4.7 -Isabelle-specific implementation of quasi-abstract markup elements.
     4.8 +Quasi-abstract markup elements.
     4.9  */
    4.10  
    4.11  package isabelle
    4.12 @@ -10,6 +10,30 @@
    4.13  
    4.14  object Markup
    4.15  {
    4.16 +  /* elements */
    4.17 +
    4.18 +  object Elements
    4.19 +  {
    4.20 +    def apply(elems: Set[String]): Elements = new Elements(elems)
    4.21 +    def apply(elems: String*): Elements = apply(Set(elems: _*))
    4.22 +    val empty: Elements = apply()
    4.23 +    val full: Elements =
    4.24 +      new Elements(Set.empty)
    4.25 +      {
    4.26 +        override def apply(elem: String): Boolean = true
    4.27 +        override def toString: String = "Elements.full"
    4.28 +      }
    4.29 +  }
    4.30 +
    4.31 +  sealed class Elements private[Markup](private val rep: Set[String])
    4.32 +  {
    4.33 +    def apply(elem: String): Boolean = rep.contains(elem)
    4.34 +    def + (elem: String): Elements = new Elements(rep + elem)
    4.35 +    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
    4.36 +    override def toString: String = rep.mkString("Elements(", ",", ")")
    4.37 +  }
    4.38 +
    4.39 +
    4.40    /* properties */
    4.41  
    4.42    val NAME = "name"
     5.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Apr 26 06:43:06 2014 +0200
     5.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Apr 26 13:07:20 2014 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  
     5.5    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
     5.6  
     5.7 -  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
     5.8 +  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
     5.9      (empty /: trees)(_.merge(_, range, elements))
    5.10  
    5.11    def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    5.12 @@ -54,7 +54,7 @@
    5.13    {
    5.14      def markup: List[XML.Elem] = rev_markup.reverse
    5.15  
    5.16 -    def filter_markup(elements: Document.Elements): List[XML.Elem] =
    5.17 +    def filter_markup(elements: Markup.Elements): List[XML.Elem] =
    5.18      {
    5.19        var result: List[XML.Elem] = Nil
    5.20        for { elem <- rev_markup; if (elements(elem.name)) }
    5.21 @@ -161,7 +161,7 @@
    5.22      }
    5.23    }
    5.24  
    5.25 -  def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
    5.26 +  def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
    5.27    {
    5.28      def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
    5.29        (tree1 /: tree2.branches)(
    5.30 @@ -181,7 +181,7 @@
    5.31      }
    5.32    }
    5.33  
    5.34 -  def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
    5.35 +  def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
    5.36      result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    5.37    {
    5.38      def results(x: A, entry: Entry): Option[A] =
    5.39 @@ -230,7 +230,7 @@
    5.40        List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
    5.41    }
    5.42  
    5.43 -  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
    5.44 +  def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
    5.45    {
    5.46      def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
    5.47        if (start == stop) Nil
     6.1 --- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 06:43:06 2014 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:07:20 2014 +0200
     6.3 @@ -101,7 +101,7 @@
     6.4    }
     6.5  
     6.6    val proper_status_elements =
     6.7 -    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     6.8 +    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     6.9        Markup.FINISHED, Markup.FAILED)
    6.10  
    6.11    val liberal_status_elements =
    6.12 @@ -187,7 +187,7 @@
    6.13    /* result messages */
    6.14  
    6.15    private val clean_elements =
    6.16 -    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
    6.17 +    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    6.18  
    6.19    def clean_message(body: XML.Body): XML.Body =
    6.20      body filter {
    6.21 @@ -308,7 +308,7 @@
    6.22    /* reported positions */
    6.23  
    6.24    private val position_elements =
    6.25 -    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    6.26 +    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    6.27  
    6.28    def message_positions(
    6.29      self_id: Document_ID.Generic => Boolean,
     7.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Apr 26 06:43:06 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Apr 26 13:07:20 2014 +0200
     7.3 @@ -162,7 +162,7 @@
     7.4            val markup =
     7.5              snapshot.state.command_markup(
     7.6                snapshot.version, command, Command.Markup_Index.markup,
     7.7 -                command.range, Document.Elements.full)
     7.8 +                command.range, Markup.Elements.full)
     7.9            Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
    7.10                {
    7.11                  val range = info.range + command_start
     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Apr 26 06:43:06 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Apr 26 13:07:20 2014 +0200
     8.3 @@ -129,28 +129,28 @@
     8.4    /* markup elements */
     8.5  
     8.6    private val semantic_completion_elements =
     8.7 -    Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
     8.8 +    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
     8.9  
    8.10    private val language_context_elements =
    8.11 -    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    8.12 +    Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    8.13        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
    8.14        Markup.ML_STRING, Markup.ML_COMMENT)
    8.15  
    8.16    private val highlight_elements =
    8.17 -    Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    8.18 +    Markup.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    8.19        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    8.20        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    8.21        Markup.VAR, Markup.TFREE, Markup.TVAR)
    8.22  
    8.23    private val hyperlink_elements =
    8.24 -    Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    8.25 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    8.26  
    8.27    private val active_elements =
    8.28 -    Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    8.29 +    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    8.30        Markup.SENDBACK, Markup.SIMP_TRACE)
    8.31  
    8.32    private val tooltip_message_elements =
    8.33 -    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    8.34 +    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    8.35  
    8.36    private val tooltip_descriptions =
    8.37      Map(
    8.38 @@ -163,23 +163,23 @@
    8.39        Markup.TVAR -> "schematic type variable")
    8.40  
    8.41    private val tooltip_elements =
    8.42 -    Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    8.43 +    Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    8.44        Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    8.45 -    Document.Elements(tooltip_descriptions.keySet)
    8.46 +    Markup.Elements(tooltip_descriptions.keySet)
    8.47  
    8.48    private val gutter_elements =
    8.49 -    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    8.50 +    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    8.51  
    8.52    private val squiggly_elements =
    8.53 -    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    8.54 +    Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    8.55  
    8.56    private val line_background_elements =
    8.57 -    Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    8.58 +    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    8.59        Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
    8.60        Markup.INFORMATION)
    8.61  
    8.62    private val separator_elements =
    8.63 -    Document.Elements(Markup.SEPARATOR)
    8.64 +    Markup.Elements(Markup.SEPARATOR)
    8.65  
    8.66    private val background_elements =
    8.67      Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    8.68 @@ -188,14 +188,14 @@
    8.69        active_elements
    8.70  
    8.71    private val foreground_elements =
    8.72 -    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    8.73 +    Markup.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    8.74        Markup.CARTOUCHE, Markup.ANTIQUOTED)
    8.75  
    8.76    private val bullet_elements =
    8.77 -    Document.Elements(Markup.BULLET)
    8.78 +    Markup.Elements(Markup.BULLET)
    8.79  
    8.80    private val fold_depth_elements =
    8.81 -    Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    8.82 +    Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    8.83  }
    8.84  
    8.85  
    8.86 @@ -287,7 +287,7 @@
    8.87    /* spell checker */
    8.88  
    8.89    private lazy val spell_checker_elements =
    8.90 -    Document.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
    8.91 +    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
    8.92  
    8.93    def spell_checker_ranges(range: Text.Range): List[Text.Range] =
    8.94      snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
    8.95 @@ -407,7 +407,7 @@
    8.96  
    8.97    def command_results(range: Text.Range): Command.Results =
    8.98      Command.State.merge_results(
    8.99 -      snapshot.select[List[Command.State]](range, Document.Elements.full, command_states =>
   8.100 +      snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
   8.101          { case _ => Some(command_states) }).flatMap(_.info))
   8.102  
   8.103  
   8.104 @@ -695,7 +695,7 @@
   8.105        Markup.SML_COMMENT -> inner_comment_color)
   8.106  
   8.107    private lazy val text_color_elements =
   8.108 -    Document.Elements(text_colors.keySet)
   8.109 +    Markup.Elements(text_colors.keySet)
   8.110  
   8.111    def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   8.112    {