From 174089817148eba8d6ac3f855d7b2f4eecb193bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 1 Mar 2024 17:24:12 +0100 Subject: [PATCH] Add message for matching error in class invariants Give feedback for not well formed class invariants --- Isabelle_DOF/thys/Isa_DOF.thy | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 0c7dc2c..ccc5ff3 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -1821,7 +1821,12 @@ fun check_invariants thy binding = let val ctxt = Proof_Context.init_global thy val trivial_true = \<^term>\True\ |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial val evaluated_term = value ctxt term - handle ERROR e => + handle Match => error ("exception Match raised when checking " + ^ inv_name ^ " invariant." ^ Position.here pos ^ "\n" + ^ "You might want to check the definition of the invariant\n" + ^ "against the value specified in the instance\n" + ^ "or the default value declared in the instance class.") + | ERROR e => if (String.isSubstring "Wellsortedness error" e) andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics) then (warning("Invariants checking uses proof tactics");