changeset 38413 | 224efb14f258 |
parent 38374 | 7eb0f6991e25 |
child 38414 | 49f1f657adc2 |
--- a/src/Pure/System/session.scala Sat Aug 14 18:43:45 2010 +0200 +++ b/src/Pure/System/session.scala Sat Aug 14 21:25:20 2010 +0200 @@ -153,7 +153,6 @@ case None => if (result.is_status) { result.body match { - // keyword declarations // FIXME always global!? case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name case _ => if (!result.is_ready) bad_result(result)