proper markup for target language code

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 30 11:21:32 2025 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 30 11:21:34 2025 +0200
@@ -2291,26 +2291,28 @@
     ;
     symbol_module: @'code_module' name
     ;
-    syntax: @{syntax string} | (@'infix' | @'infixl' | @'infixr')
-      @{syntax nat} @{syntax string}
+    target_syntax: @{syntax embedded}
+    ;
+    rich_syntax: target_syntax | (@'infix' | @'infixl' | @'infixr')
+      @{syntax nat} target_syntax
     ;
     printing_const: symbol_const ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' syntax ? + @'and')
+      ('(' target ')' rich_syntax ? + @'and')
     ;
     printing_type_constructor: symbol_type_constructor ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' syntax ? + @'and')
+      ('(' target ')' rich_syntax ? + @'and')
     ;
     printing_class: symbol_class ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' @{syntax string} ? + @'and')
+      ('(' target ')' target_syntax ? + @'and')
     ;
     printing_class_relation: symbol_class_relation ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' @{syntax string} ? + @'and')
+      ('(' target ')' target_syntax ? + @'and')
     ;
     printing_class_instance: symbol_class_instance ('\<rightharpoonup>'| '=>') \<newline>
       ('(' target ')' '-' ? + @'and')
     ;
     printing_module: symbol_module ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' (@{syntax string} for_symbol?)? + @'and')
+      ('(' target ')' (target_syntax for_symbol?)? + @'and')
     ;
     for_symbol:
       @'for'

--- a/src/Tools/Code/code_printer.ML	Sun Mar 30 11:21:32 2025 +0200
+++ b/src/Tools/Code/code_printer.ML	Sun Mar 30 11:21:34 2025 +0200
@@ -64,6 +64,7 @@
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
+  val parse_target_source: string parser
   type raw_const_syntax
   val plain_const_syntax: string -> raw_const_syntax
   type simple_const_syntax
@@ -282,6 +283,26 @@
 
 (* generic syntax *)
 
+local
+
+val target = Markup.language'
+  {name = "code target language", symbols = false, antiquotes = false};
+
+fun markup_target source =
+  let
+    val pos = Input.pos_of source;
+    val _ =
+      if Position.is_reported_range pos
+      then Position.report pos (target (Input.is_delimited source))
+      else ();
+  in Input.string_of source end;
+
+in
+
+val parse_target_source = Parse.input Parse.embedded >> markup_target;
+
+end
+
 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   -> fixity -> (iterm * itype) list -> Pretty.T);
 
@@ -400,8 +421,8 @@
   (\<^keyword>\<open>infix\<close> >> K X) || (\<^keyword>\<open>infixl\<close> >> K L) || (\<^keyword>\<open>infixr\<close> >> K R)
 
 fun parse_mixfix x =
-  (Parse.string >> read_mixfix
-  || parse_fixity -- Parse.nat -- Parse.string
+  (parse_target_source >> read_mixfix
+  || parse_fixity -- Parse.nat -- parse_target_source
      >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x;
 
 fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s

--- 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 _ =