src/Tools/Code/code_target.ML

 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
 
 
 (* custom printings *)
 
-fun arrange_printings prep_syms ctxt =
+datatype target_source = Literal of string | File of Path.T
+
+local
+
+val format_source = Pretty.block0 o Pretty.fbreaks o map Code_Printer.str o split_lines;
+
+fun eval_source (Literal s) = s
+  | eval_source (File p) = File.read p;
+
+fun arrange_printings prep_syms prep_source ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun arrange check (sym, target_syns) =
       map (fn (target_name, some_syn) =>
         (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)
         (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
-        (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) =>
-          (Pretty.block0 (Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
-            map (prep_syms ctxt) raw_syms)))
-  end;
-
-fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms ctxt;
-
-fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms ctxt;
+        (arrange (fn ctxt => fn _ => fn _ => fn (source, raw_syms) =>
+          (format_source (prep_source source), map (prep_syms ctxt) raw_syms)))
+  end;
+
+fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms I ctxt;
+
+fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms eval_source ctxt;
 
 fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn);
 
 fun gen_set_printings prep_print_decl raw_print_decls thy =
   fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
 
+in
+
 val set_printings = gen_set_printings cert_printings;
 val set_printings_cmd = gen_set_printings read_printings;
+
+end;
 
 
 (* concrete syntax *)
 
 fun parse_args f args =

 
 fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
     (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
 
+val parse_target_source = Code_Printer.parse_target_source >> Literal
+  || \<^keyword>\<open>file\<close> |-- Parse.path >> (File o Path.explode);
+
 val code_expr_argsP = Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.args --| \<^keyword>\<open>)\<close>) [];
 
 fun code_expr_inP (all_public, raw_cs) =
   Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name
     -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""

 
 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)
       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) [])
+      (parse_target_source -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
       >> (Toplevel.theory o fold set_printings_cmd));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>export_code\<close> "generate executable code for constants"
     (Scan.optional (\<^keyword>\<open>open\<close> >> K true) false -- Scan.repeat1 Parse.term