--- a/src/Pure/General/completion.scala Tue Aug 02 18:58:49 2016 +0200
+++ b/src/Pure/General/completion.scala Tue Aug 02 21:04:52 2016 +0200
@@ -249,7 +249,7 @@
/* word parsers */
- private object Word_Parsers extends RegexParsers
+ object Word_Parsers extends RegexParsers
{
override val whiteSpace = "".r
--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 02 18:58:49 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 02 21:04:52 2016 +0200
@@ -89,10 +89,11 @@
{
val keywords1 = keywords + (name, kind, tags)
val completion1 =
- completion.add_keyword(name).add_abbrevs(
- if (Keyword.theory_block.contains(kind))
- List((name, name + "\nbegin\n\u0007\nend"), (name, name))
- else List((name, name)))
+ completion.add_keyword(name).
+ add_abbrevs(
+ (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
+ else Nil) :::
+ (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
new Outer_Syntax(keywords1, completion1, language_context, true)
}