# HG changeset patch # User wenzelm # Date 1261219691 -3600 # Node ID 63dd95e3b39325e2cbc67375726326d2308de66f # Parent d8d9df8407f65a2a35d8ed753e3774a7fdfa3004 indicate final state of keywords; added symbol scanner; diff -r d8d9df8407f6 -r 63dd95e3b393 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Sat Dec 19 11:45:14 2009 +0100 +++ b/src/Pure/General/scan.scala Sat Dec 19 11:48:11 2009 +0100 @@ -91,7 +91,8 @@ Tree(tree.branches + (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1)))) } - } else tree + } + else tree val old = this new Lexicon { override val main_tree = extend(old.main_tree, 0) } } @@ -106,28 +107,45 @@ override val whiteSpace = "".r - def keyword: Parser[String] = new Parser[String] { + type Result = (String, Boolean) + + def keyword: Parser[Result] = new Parser[Result] + { def apply(in: Input) = { val source = in.source val offset = in.offset val len = source.length - offset - def scan(tree: Tree, text: String, i: Int): String = + def scan(tree: Tree, result: Result, i: Int): Result = { if (i < len) { tree.branches.get(source.charAt(offset + i)) match { - case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1) - case None => text + case Some((s, tr)) => + scan(tr, if (s.isEmpty) result else (s, tr.branches.isEmpty), i + 1) + case None => result } - } else text + } + else result } - val text = scan(main_tree, "", 0) + val result @ (text, terminated) = scan(main_tree, ("", false), 0) if (text.isEmpty) Failure("keyword expected", in) - else Success(text, in.drop(text.length)) + else Success(result, in.drop(text.length)) } }.named("keyword") + def symbol: Parser[String] = new Parser[String] + { + private val symbol_regex = regex(Symbol.regex) + def apply(in: Input) = + { + val source = in.source + val offset = in.offset + if (offset >= source.length) Failure("input expected", in) + else if (Symbol.could_open(source.charAt(offset))) symbol_regex(in) + else Success(source.subSequence(offset, offset + 1).toString, in.drop(1)) + } + }.named("symbol") } } diff -r d8d9df8407f6 -r 63dd95e3b393 src/Pure/Thy/completion.scala --- a/src/Pure/Thy/completion.scala Sat Dec 19 11:45:14 2009 +0100 +++ b/src/Pure/Thy/completion.scala Sat Dec 19 11:48:11 2009 +0100 @@ -114,7 +114,7 @@ def complete(line: CharSequence): Option[(String, List[String])] = { abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match { - case abbrevs_lex.Success(rev_a, _) => + case abbrevs_lex.Success((rev_a, _), _) => val (word, c) = abbrevs_map(rev_a) if (word == c) None else Some(word, List(c))