# HG changeset patch # User wenzelm # Date 1417443709 -3600 # Node ID dcecfcc56dced1faa75e09935ca039132f0f0700 # Parent 27c6936c6484c667f71bd9b4a37a6a5f6d83d411 more merge operations; diff -r 27c6936c6484 -r dcecfcc56dce src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Mon Dec 01 14:24:05 2014 +0100 +++ b/src/Pure/General/completion.scala Mon Dec 01 15:21:49 2014 +0100 @@ -276,12 +276,35 @@ } final class Completion private( - keywords: Map[String, Boolean] = Map.empty, - words_lex: Scan.Lexicon = Scan.Lexicon.empty, - words_map: Multi_Map[String, String] = Multi_Map.empty, - abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, - abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) + protected val keywords: Map[String, Boolean] = Map.empty, + protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty, + protected val words_map: Multi_Map[String, String] = Multi_Map.empty, + protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, + protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) { + /* merge */ + + def is_empty: Boolean = + keywords.isEmpty && + words_lex.is_empty && + words_map.isEmpty && + abbrevs_lex.is_empty && + abbrevs_map.isEmpty + + def ++ (other: Completion): Completion = + if (this eq other) this + else if (is_empty) other + else { + val keywords1 = + (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } + val words_lex1 = words_lex ++ other.words_lex + val words_map1 = words_map ++ other.words_map + val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex + val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map + new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) + } + + /* keywords */ private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name) diff -r 27c6936c6484 -r dcecfcc56dce src/Pure/General/multi_map.scala --- a/src/Pure/General/multi_map.scala Mon Dec 01 14:24:05 2014 +0100 +++ b/src/Pure/General/multi_map.scala Mon Dec 01 15:21:49 2014 +0100 @@ -21,7 +21,7 @@ } -final class Multi_Map[A, +B] private(rep: Map[A, List[B]]) +final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]]) extends scala.collection.immutable.Map[A, B] with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]] { @@ -50,6 +50,14 @@ else this } + def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] = + if (this eq other) this + else if (isEmpty) other + else + (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) { + case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) } + } + /* Map operations */ diff -r 27c6936c6484 -r dcecfcc56dce src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Mon Dec 01 14:24:05 2014 +0100 +++ b/src/Pure/General/scan.scala Mon Dec 01 15:21:49 2014 +0100 @@ -318,10 +318,10 @@ { /* auxiliary operations */ - private def content(tree: Lexicon.Tree, result: List[String]): List[String] = + private def dest(tree: Lexicon.Tree, result: List[String]): List[String] = (result /: tree.branches.toList) ((res, entry) => entry match { case (_, (s, tr)) => - if (s.isEmpty) content(tr, res) else content(tr, s :: res) }) + if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) }) private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = { @@ -341,20 +341,20 @@ def completions(str: CharSequence): List[String] = lookup(str) match { - case Some((true, tree)) => content(tree, List(str.toString)) - case Some((false, tree)) => content(tree, Nil) + case Some((true, tree)) => dest(tree, List(str.toString)) + case Some((false, tree)) => dest(tree, Nil) case None => Nil } /* pseudo Set methods */ - def iterator: Iterator[String] = content(rep, Nil).sorted.iterator + def raw_iterator: Iterator[String] = dest(rep, Nil).iterator + def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator override def toString: String = iterator.mkString("Lexicon(", ", ", ")") - def empty: Lexicon = Lexicon.empty - def isEmpty: Boolean = rep.branches.isEmpty + def is_empty: Boolean = rep.branches.isEmpty def contains(elem: String): Boolean = lookup(elem) match { @@ -363,7 +363,7 @@ } - /* add elements */ + /* build lexicon */ def + (elem: String): Lexicon = if (contains(elem)) this @@ -388,6 +388,11 @@ def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _) + def ++ (other: Lexicon): Lexicon = + if (this eq other) this + else if (is_empty) other + else this ++ other.raw_iterator + /* scan */ diff -r 27c6936c6484 -r dcecfcc56dce src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Mon Dec 01 14:24:05 2014 +0100 +++ b/src/Pure/Isar/keyword.scala Mon Dec 01 15:21:49 2014 +0100 @@ -83,12 +83,8 @@ class Keywords private( val minor: Scan.Lexicon = Scan.Lexicon.empty, val major: Scan.Lexicon = Scan.Lexicon.empty, - commands: Map[String, (String, List[String])] = Map.empty) + protected val commands: Map[String, (String, List[String])] = Map.empty) { - /* content */ - - def is_empty: Boolean = minor.isEmpty && major.isEmpty - override def toString: String = { val keywords1 = minor.iterator.map(quote(_)).toList @@ -101,6 +97,24 @@ } + /* merge */ + + def is_empty: Boolean = minor.is_empty && major.is_empty + + def ++ (other: Keywords): Keywords = + if (this eq other) this + else if (is_empty) other + else { + val minor1 = minor ++ other.minor + val major1 = major ++ other.major + val commands1 = + if (commands eq other.commands) commands + else if (commands.isEmpty) other.commands + else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } + new Keywords(minor1, major1, commands1) + } + + /* add keywords */ def + (name: String): Keywords = new Keywords(minor + name, major, commands) diff -r 27c6936c6484 -r dcecfcc56dce src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Mon Dec 01 14:24:05 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Mon Dec 01 15:21:49 2014 +0100 @@ -112,6 +112,17 @@ } + /* merge */ + + def ++ (other: Outer_Syntax): Outer_Syntax = + if (this eq other) this + else { + val keywords1 = keywords ++ other.keywords + val completion1 = completion ++ other.completion + new Outer_Syntax(keywords1, completion1, language_context, has_tokens) + } + + /* load commands */ def load_command(name: String): Option[List[String]] = keywords.load_command(name)