--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 07 15:01:48 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 07 15:19:08 2012 +0200
@@ -62,8 +62,10 @@
def add_keywords(header: Document.Node.Header): Outer_Syntax =
(this /: header.keywords) {
- case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
- case (syntax, ((name, None))) => syntax + name
+ case (syntax, ((name, Some((kind, _))))) =>
+ syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
+ case (syntax, ((name, None))) =>
+ syntax + Symbol.decode(name) + Symbol.encode(name)
}
def is_command(name: String): Boolean =