1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Aug 12 21:27:57 2008 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Aug 12 21:27:59 2008 +0200
     1.3 @@ -57,6 +57,8 @@
     1.4    val keep: (state -> unit) -> transition -> transition
     1.5    val keep': (bool -> state -> unit) -> transition -> transition
     1.6    val imperative: (unit -> unit) -> transition -> transition
     1.7 +  val ignored: Position.T -> transition
     1.8 +  val malformed: Position.T -> string -> transition
     1.9    val theory: (theory -> theory) -> transition -> transition
    1.10    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    1.11    val theory': (bool -> theory -> theory) -> transition -> transition
    1.12 @@ -460,6 +462,10 @@
    1.13  fun keep f = add_trans (Keep (fn _ => f));
    1.14  fun imperative f = keep (fn _ => f ());
    1.15  
    1.16 +fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    1.17 +fun malformed pos msg =
    1.18 +  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    1.19 +
    1.20  val unknown_theory = imperative (fn () => warning "Unknown theory context");
    1.21  val unknown_proof = imperative (fn () => warning "Unknown proof context");
    1.22  val unknown_context = imperative (fn () => warning "Unknown context");