src/Pure/Isar/outer_keyword.ML
changeset 28345 4562584d9d66
parent 27805 2e533bcd1343
child 28431 f12c1c68ec8e
equal deleted inserted replaced
28344:f4a17868bde5 28345:4562584d9d66
   146 
   146 
   147 fun report () =
   147 fun report () =
   148   let val (keywords, commands) = CRITICAL (fn () =>
   148   let val (keywords, commands) = CRITICAL (fn () =>
   149     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   149     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   150   in map report_keyword keywords @ map report_command commands end
   150   in map report_keyword keywords @ map report_command commands end
   151   |> Pretty.chunks |> Pretty.string_of |> Output.status;
   151   |> List.app (Output.status o Pretty.string_of);
   152 
   152 
   153 
   153 
   154 (* augment tables *)
   154 (* augment tables *)
   155 
   155 
   156 fun keyword name =
   156 fun keyword name =