Keyword.status: always suppress position;
authorwenzelm
Sat Aug 14 21:25:20 2010 +0200 (2010-08-14)
changeset 38413224efb14f258
parent 38412 c23f3abbf42d
child 38414 49f1f657adc2
Keyword.status: always suppress position;
src/Pure/Isar/keyword.ML
src/Pure/System/session.scala
     1.1 --- a/src/Pure/Isar/keyword.ML	Sat Aug 14 18:43:45 2010 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Sat Aug 14 21:25:20 2010 +0200
     1.3 @@ -151,7 +151,8 @@
     1.4  val keyword_statusN = "keyword_status";
     1.5  
     1.6  fun status_message s =
     1.7 -  (if print_mode_active keyword_statusN then Output.status else writeln) s;
     1.8 +  Position.setmp_thread_data Position.none
     1.9 +    (if print_mode_active keyword_statusN then Output.status else writeln) s;
    1.10  
    1.11  fun keyword_status name =
    1.12    status_message (Markup.markup (Markup.keyword_decl name)
     2.1 --- a/src/Pure/System/session.scala	Sat Aug 14 18:43:45 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 21:25:20 2010 +0200
     2.3 @@ -153,7 +153,6 @@
     2.4          case None =>
     2.5            if (result.is_status) {
     2.6              result.body match {
     2.7 -              // keyword declarations   // FIXME always global!?
     2.8                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
     2.9                case List(Keyword.Keyword_Decl(name)) => syntax += name
    2.10                case _ => if (!result.is_ready) bad_result(result)