# 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 "" |> position pos |> imperative I; +fun malformed pos msg = + empty |> name "" |> 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");