src/Pure/Isar/toplevel.ML
changeset 48772 e46cd0d26481
parent 48633 7cd32f9d4293
child 48992 0518bf89c777
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 11 18:05:41 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 11 19:34:36 2012 +0200
     1.3 @@ -53,6 +53,7 @@
     1.4    val imperative: (unit -> unit) -> transition -> transition
     1.5    val ignored: Position.T -> transition
     1.6    val malformed: Position.T -> string -> transition
     1.7 +  val is_malformed: transition -> bool
     1.8    val theory: (theory -> theory) -> transition -> transition
     1.9    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    1.10    val theory': (bool -> theory -> theory) -> transition -> transition
    1.11 @@ -412,8 +413,11 @@
    1.12  fun imperative f = keep (fn _ => f ());
    1.13  
    1.14  fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    1.15 +
    1.16 +val malformed_name = "<malformed>";
    1.17  fun malformed pos msg =
    1.18 -  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    1.19 +  empty |> name malformed_name |> position pos |> imperative (fn () => error msg);
    1.20 +fun is_malformed tr = name_of tr = malformed_name;
    1.21  
    1.22  val unknown_theory = imperative (fn () => warning "Unknown theory context");
    1.23  val unknown_proof = imperative (fn () => warning "Unknown proof context");