# HG changeset patch
# User wenzelm
# Date 1635952789 -3600
# Node ID 1a8fd26fedb636e30d001ab89ad87f314c5bd2f6
# Parent  df12779c3ce8fa0da55cd34c10a1fc9853e0e052
tuned signature;

diff -r df12779c3ce8 -r 1a8fd26fedb6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Nov 03 14:26:13 2021 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Nov 03 16:19:49 2021 +0100
@@ -48,6 +48,7 @@
   val keep': (bool -> state -> unit) -> transition -> transition
   val keep_proof: (state -> unit) -> transition -> transition
   val is_ignored: transition -> bool
+  val is_malformed: transition -> bool
   val ignored: Position.T -> transition
   val malformed: Position.T -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
@@ -416,13 +417,17 @@
     else if is_skipped_proof st then ()
     else warning "No proof state");
 
-fun is_ignored tr = name_of tr = "<ignored>";
+val ignoredN = "<ignored>";
+val malformedN = "<malformed>";
+
+fun is_ignored tr = name_of tr = ignoredN;
+fun is_malformed tr = name_of tr = malformedN;
 
 fun ignored pos =
-  empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
+  empty |> name ignoredN |> position pos |> keep (fn _ => ());
 
 fun malformed pos msg =
-  empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg);
+  empty |> name malformedN |> position pos |> keep (fn _ => error msg);
 
 
 (* theory transitions *)