# HG changeset patch
# User wenzelm
# Date 1218569279 -7200
# Node ID e9483ef084ccc9a7478a8358ba707f6aab935f11
# Parent  0be8644c45eb5a65066eaca8fe236de28984997f
added ignored, malformed transitions;

diff -r 0be8644c45eb -r e9483ef084cc src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Aug 12 21:27:57 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Aug 12 21:27:59 2008 +0200
@@ -57,6 +57,8 @@
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
+  val ignored: Position.T -> transition
+  val malformed: Position.T -> string -> transition
   val theory: (theory -> theory) -> transition -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
@@ -460,6 +462,10 @@
 fun keep f = add_trans (Keep (fn _ => f));
 fun imperative f = keep (fn _ => f ());
 
+fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
+fun malformed pos msg =
+  empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
+
 val unknown_theory = imperative (fn () => warning "Unknown theory context");
 val unknown_proof = imperative (fn () => warning "Unknown proof context");
 val unknown_context = imperative (fn () => warning "Unknown context");