--- a/src/Pure/Isar/keyword.ML Sat Aug 14 18:43:45 2010 +0200
+++ b/src/Pure/Isar/keyword.ML Sat Aug 14 21:25:20 2010 +0200
@@ -151,7 +151,8 @@
val keyword_statusN = "keyword_status";
fun status_message s =
- (if print_mode_active keyword_statusN then Output.status else writeln) s;
+ Position.setmp_thread_data Position.none
+ (if print_mode_active keyword_statusN then Output.status else writeln) s;
fun keyword_status name =
status_message (Markup.markup (Markup.keyword_decl name)
--- 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)