# HG changeset patch
# User wenzelm
# Date 1281813920 -7200
# Node ID 224efb14f258601f29b9ffcb9aa0640b2eb9b8cb
# Parent  c23f3abbf42db1211f6f50114bed2d3a34f33303
Keyword.status: always suppress position;

diff -r c23f3abbf42d -r 224efb14f258 src/Pure/Isar/keyword.ML
--- 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)
diff -r c23f3abbf42d -r 224efb14f258 src/Pure/System/session.scala
--- 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)