explicit error message for non-existing code target
authorhaftmann
Thu, 02 Jan 2025 08:37:52 +0100
changeset 81705 53fea2ccab19
parent 81704 9253dadbd4ac
child 81706 7beb0cf38292
explicit error message for non-existing code target
src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Jan 01 22:06:27 2025 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Jan 02 08:37:52 2025 +0100
@@ -643,9 +643,10 @@
 
 fun arrange_printings prep_syms ctxt =
   let
+    val thy = Proof_Context.theory_of ctxt;
     fun arrange check (sym, target_syns) =
       map (fn (target_name, some_syn) =>
-        (target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns;
+        (assert_target thy target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns;
   in
     Code_Symbol.maps_attr'
       (arrange check_const_syntax) (arrange check_tyco_syntax)