more merge operations;
authorwenzelm
Mon Dec 01 15:21:49 2014 +0100 (2014-12-01)
changeset 59073dcecfcc56dce
parent 59072 27c6936c6484
child 59074 7836d927ffca
more merge operations;
src/Pure/General/completion.scala
src/Pure/General/multi_map.scala
src/Pure/General/scan.scala
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/General/completion.scala	Mon Dec 01 14:24:05 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Mon Dec 01 15:21:49 2014 +0100
     1.3 @@ -276,12 +276,35 @@
     1.4  }
     1.5  
     1.6  final class Completion private(
     1.7 -  keywords: Map[String, Boolean] = Map.empty,
     1.8 -  words_lex: Scan.Lexicon = Scan.Lexicon.empty,
     1.9 -  words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.10 -  abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.11 -  abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
    1.12 +  protected val keywords: Map[String, Boolean] = Map.empty,
    1.13 +  protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.14 +  protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.15 +  protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.16 +  protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
    1.17  {
    1.18 +  /* merge */
    1.19 +
    1.20 +  def is_empty: Boolean =
    1.21 +    keywords.isEmpty &&
    1.22 +    words_lex.is_empty &&
    1.23 +    words_map.isEmpty &&
    1.24 +    abbrevs_lex.is_empty &&
    1.25 +    abbrevs_map.isEmpty
    1.26 +
    1.27 +  def ++ (other: Completion): Completion =
    1.28 +    if (this eq other) this
    1.29 +    else if (is_empty) other
    1.30 +    else {
    1.31 +      val keywords1 =
    1.32 +        (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    1.33 +      val words_lex1 = words_lex ++ other.words_lex
    1.34 +      val words_map1 = words_map ++ other.words_map
    1.35 +      val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
    1.36 +      val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
    1.37 +      new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    1.38 +    }
    1.39 +
    1.40 +
    1.41    /* keywords */
    1.42  
    1.43    private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
     2.1 --- a/src/Pure/General/multi_map.scala	Mon Dec 01 14:24:05 2014 +0100
     2.2 +++ b/src/Pure/General/multi_map.scala	Mon Dec 01 15:21:49 2014 +0100
     2.3 @@ -21,7 +21,7 @@
     2.4  }
     2.5  
     2.6  
     2.7 -final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
     2.8 +final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]])
     2.9    extends scala.collection.immutable.Map[A, B]
    2.10    with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
    2.11  {
    2.12 @@ -50,6 +50,14 @@
    2.13      else this
    2.14    }
    2.15  
    2.16 +  def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] =
    2.17 +    if (this eq other) this
    2.18 +    else if (isEmpty) other
    2.19 +    else
    2.20 +      (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
    2.21 +        case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
    2.22 +      }
    2.23 +
    2.24  
    2.25    /* Map operations */
    2.26  
     3.1 --- a/src/Pure/General/scan.scala	Mon Dec 01 14:24:05 2014 +0100
     3.2 +++ b/src/Pure/General/scan.scala	Mon Dec 01 15:21:49 2014 +0100
     3.3 @@ -318,10 +318,10 @@
     3.4    {
     3.5      /* auxiliary operations */
     3.6  
     3.7 -    private def content(tree: Lexicon.Tree, result: List[String]): List[String] =
     3.8 +    private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
     3.9        (result /: tree.branches.toList) ((res, entry) =>
    3.10          entry match { case (_, (s, tr)) =>
    3.11 -          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
    3.12 +          if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
    3.13  
    3.14      private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
    3.15      {
    3.16 @@ -341,20 +341,20 @@
    3.17  
    3.18      def completions(str: CharSequence): List[String] =
    3.19        lookup(str) match {
    3.20 -        case Some((true, tree)) => content(tree, List(str.toString))
    3.21 -        case Some((false, tree)) => content(tree, Nil)
    3.22 +        case Some((true, tree)) => dest(tree, List(str.toString))
    3.23 +        case Some((false, tree)) => dest(tree, Nil)
    3.24          case None => Nil
    3.25        }
    3.26  
    3.27  
    3.28      /* pseudo Set methods */
    3.29  
    3.30 -    def iterator: Iterator[String] = content(rep, Nil).sorted.iterator
    3.31 +    def raw_iterator: Iterator[String] = dest(rep, Nil).iterator
    3.32 +    def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator
    3.33  
    3.34      override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
    3.35  
    3.36 -    def empty: Lexicon = Lexicon.empty
    3.37 -    def isEmpty: Boolean = rep.branches.isEmpty
    3.38 +    def is_empty: Boolean = rep.branches.isEmpty
    3.39  
    3.40      def contains(elem: String): Boolean =
    3.41        lookup(elem) match {
    3.42 @@ -363,7 +363,7 @@
    3.43        }
    3.44  
    3.45  
    3.46 -    /* add elements */
    3.47 +    /* build lexicon */
    3.48  
    3.49      def + (elem: String): Lexicon =
    3.50        if (contains(elem)) this
    3.51 @@ -388,6 +388,11 @@
    3.52  
    3.53      def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
    3.54  
    3.55 +    def ++ (other: Lexicon): Lexicon =
    3.56 +      if (this eq other) this
    3.57 +      else if (is_empty) other
    3.58 +      else this ++ other.raw_iterator
    3.59 +
    3.60  
    3.61      /* scan */
    3.62  
     4.1 --- a/src/Pure/Isar/keyword.scala	Mon Dec 01 14:24:05 2014 +0100
     4.2 +++ b/src/Pure/Isar/keyword.scala	Mon Dec 01 15:21:49 2014 +0100
     4.3 @@ -83,12 +83,8 @@
     4.4    class Keywords private(
     4.5      val minor: Scan.Lexicon = Scan.Lexicon.empty,
     4.6      val major: Scan.Lexicon = Scan.Lexicon.empty,
     4.7 -    commands: Map[String, (String, List[String])] = Map.empty)
     4.8 +    protected val commands: Map[String, (String, List[String])] = Map.empty)
     4.9    {
    4.10 -    /* content */
    4.11 -
    4.12 -    def is_empty: Boolean = minor.isEmpty && major.isEmpty
    4.13 -
    4.14      override def toString: String =
    4.15      {
    4.16        val keywords1 = minor.iterator.map(quote(_)).toList
    4.17 @@ -101,6 +97,24 @@
    4.18      }
    4.19  
    4.20  
    4.21 +    /* merge */
    4.22 +
    4.23 +    def is_empty: Boolean = minor.is_empty && major.is_empty
    4.24 +
    4.25 +    def ++ (other: Keywords): Keywords =
    4.26 +      if (this eq other) this
    4.27 +      else if (is_empty) other
    4.28 +      else {
    4.29 +        val minor1 = minor ++ other.minor
    4.30 +        val major1 = major ++ other.major
    4.31 +        val commands1 =
    4.32 +          if (commands eq other.commands) commands
    4.33 +          else if (commands.isEmpty) other.commands
    4.34 +          else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    4.35 +        new Keywords(minor1, major1, commands1)
    4.36 +      }
    4.37 +
    4.38 +
    4.39      /* add keywords */
    4.40  
    4.41      def + (name: String): Keywords = new Keywords(minor + name, major, commands)
     5.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Dec 01 14:24:05 2014 +0100
     5.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Dec 01 15:21:49 2014 +0100
     5.3 @@ -112,6 +112,17 @@
     5.4      }
     5.5  
     5.6  
     5.7 +  /* merge */
     5.8 +
     5.9 +  def ++ (other: Outer_Syntax): Outer_Syntax =
    5.10 +    if (this eq other) this
    5.11 +    else {
    5.12 +      val keywords1 = keywords ++ other.keywords
    5.13 +      val completion1 = completion ++ other.completion
    5.14 +      new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    5.15 +    }
    5.16 +
    5.17 +
    5.18    /* load commands */
    5.19  
    5.20    def load_command(name: String): Option[List[String]] = keywords.load_command(name)