src/Tools/Code/code_target.ML
changeset 82378 23df00d48d6f
parent 81875 7fe20d394593
child 82379 3f875966c3e1
--- a/src/Tools/Code/code_target.ML	Sun Mar 30 11:21:32 2025 +0200
+++ b/src/Tools/Code/code_target.ML	Sun Mar 30 11:21:34 2025 +0200
@@ -762,8 +762,8 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_printing\<close> "declare dedicated printing for code symbols"
     (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
-      Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
-      (Parse.embedded -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
+      Code_Printer.parse_target_source (Parse.minus >> K ()) (Parse.minus >> K ())
+      (Code_Printer.parse_target_source -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
       >> (Toplevel.theory o fold set_printings_cmd));
 
 val _ =