# HG changeset patch
# User haftmann
# Date 1735803472 -3600
# Node ID 53fea2ccab1965faa50b2884cc1c1894b45c869c
# Parent  9253dadbd4aca83c2c6bd0d97d7fa8dc9b9a1147
explicit error message for non-existing code target

diff -r 9253dadbd4ac -r 53fea2ccab19 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)