src/Pure/Isar/toplevel.ML
changeset 51268 fcc4b89a600d
parent 51241 83252b0605be
child 51273 d54ee0cad2ab
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Feb 24 14:14:07 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Feb 24 17:29:55 2013 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val keep': (bool -> state -> unit) -> transition -> transition
     1.5    val imperative: (unit -> unit) -> transition -> transition
     1.6    val ignored: Position.T -> transition
     1.7 +  val is_ignored: transition -> bool
     1.8    val malformed: Position.T -> string -> transition
     1.9    val is_malformed: transition -> bool
    1.10    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    1.11 @@ -414,6 +415,7 @@
    1.12  fun imperative f = keep (fn _ => f ());
    1.13  
    1.14  fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    1.15 +fun is_ignored tr = name_of tr = "<ignored>";
    1.16  
    1.17  val malformed_name = "<malformed>";
    1.18  fun malformed pos msg =