--- 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)
--- 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 */
--- 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 */
--- 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)
--- 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)