--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/completion.scala Thu Aug 29 15:29:24 2013 +0200
@@ -0,0 +1,114 @@
+/* Title: Pure/Isar/completion.scala
+ Author: Makarius
+
+Completion of symbols and keywords.
+*/
+
+package isabelle
+
+import scala.util.parsing.combinator.RegexParsers
+
+
+object Completion
+{
+ /* items */
+
+ sealed case class Item(original: String, replacement: String, description: String)
+ { override def toString: String = description }
+
+
+ /* init */
+
+ val empty: Completion = new Completion()
+ def init(): Completion = empty.add_symbols()
+
+
+ /** word completion **/
+
+ private val word_regex = "[a-zA-Z0-9_']+".r
+ private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
+
+ private object Parse extends RegexParsers
+ {
+ override val whiteSpace = "".r
+
+ def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
+ def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
+ def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
+ def word: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
+
+ def read(in: CharSequence): Option[String] =
+ {
+ val reverse_in = new Library.Reverse(in)
+ parse((reverse_symbol | reverse_symb | escape | word) ^^ (_.reverse), reverse_in) match {
+ case Success(result, _) => Some(result)
+ case _ => None
+ }
+ }
+ }
+}
+
+final class Completion private(
+ words_lex: Scan.Lexicon = Scan.Lexicon.empty,
+ words_map: Map[String, String] = Map.empty,
+ abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
+ abbrevs_map: Map[String, (String, String)] = Map.empty)
+{
+ /* adding stuff */
+
+ def + (keyword: String, replace: String): Completion =
+ new Completion(
+ words_lex + keyword,
+ words_map + (keyword -> replace),
+ abbrevs_lex,
+ abbrevs_map)
+
+ def + (keyword: String): Completion = this + (keyword, keyword)
+
+ private def add_symbols(): Completion =
+ {
+ val words =
+ (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
+ (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList :::
+ (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList
+
+ val abbrs =
+ (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
+ yield (y.reverse.toString, (y, x))).toList
+
+ new Completion(
+ words_lex ++ words.map(_._1),
+ words_map ++ words,
+ abbrevs_lex ++ abbrs.map(_._1),
+ abbrevs_map ++ abbrs)
+ }
+
+
+ /* complete */
+
+ def complete(decode: Boolean, line: CharSequence): Option[(String, List[Completion.Item])] =
+ {
+ val raw_result =
+ abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
+ case abbrevs_lex.Success(reverse_a, _) =>
+ val (word, c) = abbrevs_map(reverse_a)
+ Some(word, List(c))
+ case _ =>
+ Completion.Parse.read(line) match {
+ case Some(word) =>
+ words_lex.completions(word).map(words_map(_)) match {
+ case Nil => None
+ case cs => Some(word, cs.sorted)
+ }
+ case None => None
+ }
+ }
+ raw_result match {
+ case Some((word, cs)) =>
+ val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
+ if (ds.isEmpty) None
+ else Some((word, ds.map(s => Completion.Item(word, s, s))))
+ case None => None
+ }
+ }
+}
--- a/src/Pure/Thy/completion.scala Thu Aug 29 15:24:36 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-/* Title: Pure/Thy/completion.scala
- Author: Makarius
-
-Completion of symbols and keywords.
-*/
-
-package isabelle
-
-import scala.util.parsing.combinator.RegexParsers
-
-
-object Completion
-{
- /* items */
-
- sealed case class Item(original: String, replacement: String, description: String)
- { override def toString: String = description }
-
-
- /* init */
-
- val empty: Completion = new Completion()
- def init(): Completion = empty.add_symbols()
-
-
- /** word completion **/
-
- private val word_regex = "[a-zA-Z0-9_']+".r
- private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
-
- private object Parse extends RegexParsers
- {
- override val whiteSpace = "".r
-
- def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
- def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
- def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
- def word: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
-
- def read(in: CharSequence): Option[String] =
- {
- val reverse_in = new Library.Reverse(in)
- parse((reverse_symbol | reverse_symb | escape | word) ^^ (_.reverse), reverse_in) match {
- case Success(result, _) => Some(result)
- case _ => None
- }
- }
- }
-}
-
-final class Completion private(
- words_lex: Scan.Lexicon = Scan.Lexicon.empty,
- words_map: Map[String, String] = Map.empty,
- abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
- abbrevs_map: Map[String, (String, String)] = Map.empty)
-{
- /* adding stuff */
-
- def + (keyword: String, replace: String): Completion =
- new Completion(
- words_lex + keyword,
- words_map + (keyword -> replace),
- abbrevs_lex,
- abbrevs_map)
-
- def + (keyword: String): Completion = this + (keyword, keyword)
-
- private def add_symbols(): Completion =
- {
- val words =
- (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
- (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList :::
- (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList
-
- val abbrs =
- (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
- yield (y.reverse.toString, (y, x))).toList
-
- new Completion(
- words_lex ++ words.map(_._1),
- words_map ++ words,
- abbrevs_lex ++ abbrs.map(_._1),
- abbrevs_map ++ abbrs)
- }
-
-
- /* complete */
-
- def complete(decode: Boolean, line: CharSequence): Option[(String, List[Completion.Item])] =
- {
- val raw_result =
- abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
- case abbrevs_lex.Success(reverse_a, _) =>
- val (word, c) = abbrevs_map(reverse_a)
- Some(word, List(c))
- case _ =>
- Completion.Parse.read(line) match {
- case Some(word) =>
- words_lex.completions(word).map(words_map(_)) match {
- case Nil => None
- case cs => Some(word, cs.sorted)
- }
- case None => None
- }
- }
- raw_result match {
- case Some((word, cs)) =>
- val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
- if (ds.isEmpty) None
- else Some((word, ds.map(s => Completion.Item(word, s, s))))
- case None => None
- }
- }
-}
--- a/src/Pure/build-jars Thu Aug 29 15:24:36 2013 +0200
+++ b/src/Pure/build-jars Thu Aug 29 15:29:24 2013 +0200
@@ -29,6 +29,7 @@
General/time.scala
General/timing.scala
General/xz_file.scala
+ Isar/completion.scala
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
@@ -64,7 +65,6 @@
System/swing_thread.scala
System/system_channel.scala
System/utf8.scala
- Thy/completion.scala
Thy/html.scala
Thy/present.scala
Thy/thy_header.scala