# HG changeset patch
# User wenzelm
# Date 1344345548 -7200
# Node ID 189ece4b4ff11db7b70417dd0f8e00b6bdf23ddd
# Parent  ba531af9114879f0e2d87482bcae307bc22b055d
permissive outer syntax wrt. symbol recoding;

diff -r ba531af91148 -r 189ece4b4ff1 src/Pure/Isar/outer_syntax.scala
--- 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 =
diff -r ba531af91148 -r 189ece4b4ff1 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Aug 07 15:01:48 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 07 15:19:08 2012 +0200
@@ -699,7 +699,6 @@
 
   /* static outer syntax */
 
-  // FIXME Symbol.decode!?
   def outer_syntax(session: String): Outer_Syntax =
   {
     val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))