# HG changeset patch
# User haftmann
# Date 1743335406 -7200
# Node ID 3f875966c3e1f05f3c8529acfbc9d29c2e80ca10
# Parent  23df00d48d6fccb3cddddcdcc94aa7c0be6c154c
optional external files as code modules

diff -r 23df00d48d6f -r 3f875966c3e1 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 30 11:21:34 2025 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 30 13:50:06 2025 +0200
@@ -2312,7 +2312,8 @@
       ('(' target ')' '-' ? + @'and')
     ;
     printing_module: symbol_module ('\<rightharpoonup>' | '=>') \<newline>
-      ('(' target ')' (target_syntax for_symbol?)? + @'and')
+      ('(' target ')' \<newline>
+        ((target_syntax | @'file' path) for_symbol?)? + @'and')
     ;
     for_symbol:
       @'for'
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Sun Mar 30 11:21:34 2025 +0200
+++ b/src/HOL/Library/Code_Lazy.thy	Sun Mar 30 13:50:06 2025 +0200
@@ -67,50 +67,8 @@
   has been evaluated to or not.
 \<close>
 
-code_printing code_module Lazy \<rightharpoonup> (SML)
-\<open>signature LAZY =
-sig
-  type 'a lazy;
-  val lazy : (unit -> 'a) -> 'a lazy;
-  val force : 'a lazy -> 'a;
-  val peek : 'a lazy -> 'a option
-  val termify_lazy : 
-   (string -> 'typerep -> 'term) -> 
-   ('term -> 'term -> 'term) -> 
-   (string -> 'typerep -> 'term -> 'term) ->
-   'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
-   ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term;
-end;
-
-structure Lazy : LAZY = 
-struct
-
-datatype 'a content =
-   Delay of unit -> 'a
- | Value of 'a 
- | Exn of exn;
-
-datatype 'a lazy = Lazy of 'a content ref;
-
-fun lazy f = Lazy (ref (Delay f));
-
-fun force (Lazy x) = case !x of
-   Delay f => (
-     let val res = f (); val _ = x := Value res; in res end
-     handle exn => (x := Exn exn; raise exn))
-  | Value x => x
-  | Exn exn => raise exn;
-
-fun peek (Lazy x) = case !x of
-    Value x => SOME x
-  | _ => NONE;
-
-fun termify_lazy const app abs unitT funT lazyT term_of T x _ =
-  app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) 
-    (case peek x of SOME y => abs "_" unitT (term_of y)
-     | _ => const "Pure.dummy_pattern" (funT unitT T));
-
-end;\<close> for type_constructor lazy constant delay force termify_lazy
+code_printing code_module Lazy \<rightharpoonup> (SML) file "~~/src/HOL/Library/Tools/lazy.ML"
+    for type_constructor lazy constant delay force termify_lazy
 | type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy"
 | constant delay \<rightharpoonup> (SML) "Lazy.lazy"
 | constant force \<rightharpoonup> (SML) "Lazy.force"
@@ -124,17 +82,8 @@
 | type_constructor lazy \<rightharpoonup> (Eval) "_ Lazy.lazy"
 | constant delay \<rightharpoonup> (Eval) "Lazy.lazy"
 | constant force \<rightharpoonup> (Eval) "Lazy.force"
-| code_module Termify_Lazy \<rightharpoonup> (Eval)
-\<open>structure Termify_Lazy = struct
-fun termify_lazy
-  (_: string -> typ -> term) (_: term -> term -> term)  (_: string -> typ -> term -> term)
-  (_: typ) (_: typ -> typ -> typ) (_: typ -> typ)
-  (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) =
-  Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $
-  (case Lazy.peek x of
-    SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x)
-  | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T));
-end;\<close> for constant termify_lazy
+| code_module Termify_Lazy \<rightharpoonup> (Eval) file "~~/src/HOL/Library/Tools/termify_lazy.ML"
+    for constant termify_lazy
 | constant termify_lazy \<rightharpoonup> (Eval) "Termify'_Lazy.termify'_lazy"
 
 code_reserved (Eval) Termify_Lazy
@@ -143,34 +92,15 @@
   type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
 | constant delay \<rightharpoonup> (OCaml) "Lazy.from'_fun"
 | constant force \<rightharpoonup> (OCaml) "Lazy.force"
-| code_module Termify_Lazy \<rightharpoonup> (OCaml)
-\<open>module Termify_Lazy : sig
-  val termify_lazy :
-   (string -> 'typerep -> 'term) ->
-   ('term -> 'term -> 'term) ->
-   (string -> 'typerep -> 'term -> 'term) ->
-   'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
-   ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term
-end = struct
-
-let termify_lazy const app abs unitT funT lazyT term_of ty x _ =
-  app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty)))
-    (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x))
-     else const "Pure.dummy_pattern" (funT unitT ty));;
-
-end;;\<close> for constant termify_lazy
+| code_module Termify_Lazy \<rightharpoonup> (OCaml) file "~~/src/HOL/Library/Tools/termify_lazy.ocaml"
+    for constant termify_lazy
 | constant termify_lazy \<rightharpoonup> (OCaml) "Termify'_Lazy.termify'_lazy"
 
 code_reserved (OCaml) Lazy Termify_Lazy
 
-
 code_printing
-  code_module Lazy \<rightharpoonup> (Haskell) \<open>
-module Lazy(Lazy, delay, force) where
-
-newtype Lazy a = Lazy a
-delay f = Lazy (f ())
-force (Lazy x) = x\<close> for type_constructor lazy constant delay force
+  code_module Lazy \<rightharpoonup> (Haskell) file "~~/src/HOL/Library/Tools/lazy.hs"
+    for type_constructor lazy constant delay force
 | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
@@ -178,43 +108,8 @@
 code_reserved (Haskell) Lazy
 
 code_printing
-  code_module Lazy \<rightharpoonup> (Scala) 
-\<open>object Lazy {
-  final class Lazy[A] (f: Unit => A) {
-    var evaluated = false;
-    lazy val x: A = f(())
-
-    def get() : A = {
-      evaluated = true;
-      return x
-    }
-  }
-
-  def force[A] (x: Lazy[A]) : A = {
-    return x.get()
-  }
-
-  def delay[A] (f: Unit => A) : Lazy[A] = {
-    return new Lazy[A] (f)
-  }
-
-  def termify_lazy[Typerep, Term, A] (
-    const: String => Typerep => Term,
-    app: Term => Term => Term,
-    abs: String => Typerep => Term => Term,
-    unitT: Typerep,
-    funT: Typerep => Typerep => Typerep,
-    lazyT: Typerep => Typerep,
-    term_of: A => Term,
-    ty: Typerep,
-    x: Lazy[A],
-    dummy: Term) : Term = {
-    x.evaluated match {
-      case true => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get())))
-      case false => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
-    }
-  }
-}\<close> for type_constructor lazy constant delay force termify_lazy
+  code_module Lazy \<rightharpoonup> (Scala) file "~~/src/HOL/Library/Tools/lazy.scala"
+    for type_constructor lazy constant delay force termify_lazy
 | type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
 | constant delay \<rightharpoonup> (Scala) "Lazy.delay"
 | constant force \<rightharpoonup> (Scala) "Lazy.force"
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/lazy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tools/lazy.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -0,0 +1,46 @@
+(* Author: Pascal Stoop, ETH Zurich
+   Author: Andreas Lochbihler, Digital Asset *)
+
+signature LAZY =
+sig
+  type 'a lazy;
+  val lazy : (unit -> 'a) -> 'a lazy;
+  val force : 'a lazy -> 'a;
+  val peek : 'a lazy -> 'a option
+  val termify_lazy :
+   (string -> 'typerep -> 'term) ->
+   ('term -> 'term -> 'term) ->
+   (string -> 'typerep -> 'term -> 'term) ->
+   'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
+   ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term;
+end;
+
+structure Lazy : LAZY =
+struct
+
+datatype 'a content =
+   Delay of unit -> 'a
+ | Value of 'a
+ | Exn of exn;
+
+datatype 'a lazy = Lazy of 'a content ref;
+
+fun lazy f = Lazy (ref (Delay f));
+
+fun force (Lazy x) = case !x of
+   Delay f => (
+     let val res = f (); val _ = x := Value res; in res end
+     handle exn => (x := Exn exn; raise exn))
+  | Value x => x
+  | Exn exn => raise exn;
+
+fun peek (Lazy x) = case !x of
+    Value x => SOME x
+  | _ => NONE;
+
+fun termify_lazy const app abs unitT funT lazyT term_of T x _ =
+  app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T)))
+    (case peek x of SOME y => abs "_" unitT (term_of y)
+     | _ => const "Pure.dummy_pattern" (funT unitT T));
+
+end;
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/lazy.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tools/lazy.hs	Sun Mar 30 13:50:06 2025 +0200
@@ -0,0 +1,8 @@
+{- Author: Pascal Stoop, ETH Zurich
+   Author: Andreas Lochbihler, Digital Asset -}
+
+module Lazy(Lazy, delay, force) where
+
+newtype Lazy a = Lazy a
+delay f = Lazy (f ())
+force (Lazy x) = x
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/lazy.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tools/lazy.scala	Sun Mar 30 13:50:06 2025 +0200
@@ -0,0 +1,39 @@
+/* Author: Pascal Stoop, ETH Zurich
+   Author: Andreas Lochbihler, Digital Asset */
+
+object Lazy {
+  final class Lazy[A] (f: Unit => A) {
+    var evaluated = false;
+    lazy val x: A = f(())
+
+    def get() : A = {
+      evaluated = true;
+      return x
+    }
+  }
+
+  def force[A] (x: Lazy[A]) : A = {
+    return x.get()
+  }
+
+  def delay[A] (f: Unit => A) : Lazy[A] = {
+    return new Lazy[A] (f)
+  }
+
+  def termify_lazy[Typerep, Term, A] (
+    const: String => Typerep => Term,
+    app: Term => Term => Term,
+    abs: String => Typerep => Term => Term,
+    unitT: Typerep,
+    funT: Typerep => Typerep => Typerep,
+    lazyT: Typerep => Typerep,
+    term_of: A => Term,
+    ty: Typerep,
+    x: Lazy[A],
+    dummy: Term) : Term = {
+    x.evaluated match {
+      case true => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get())))
+      case false => app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
+    }
+  }
+}
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/termify_lazy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tools/termify_lazy.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -0,0 +1,16 @@
+(* Author: Pascal Stoop, ETH Zurich
+   Author: Andreas Lochbihler, Digital Asset *)
+
+structure Termify_Lazy =
+struct
+
+fun termify_lazy
+  (_: string -> typ -> term) (_: term -> term -> term)  (_: string -> typ -> term -> term)
+  (_: typ) (_: typ -> typ -> typ) (_: typ -> typ)
+  (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) =
+  Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $
+  (case Lazy.peek x of
+    SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x)
+  | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T));
+
+end
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/termify_lazy.ocaml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tools/termify_lazy.ocaml	Sun Mar 30 13:50:06 2025 +0200
@@ -0,0 +1,18 @@
+(* Author: Pascal Stoop, ETH Zurich
+   Author: Andreas Lochbihler, Digital Asset *)
+
+module Termify_Lazy : sig
+  val termify_lazy :
+   (string -> 'typerep -> 'term) ->
+   ('term -> 'term -> 'term) ->
+   (string -> 'typerep -> 'term -> 'term) ->
+   'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
+   ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term
+end = struct
+
+let termify_lazy const app abs unitT funT lazyT term_of ty x _ =
+  app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty)))
+    (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x))
+     else const "Pure.dummy_pattern" (funT unitT ty));;
+
+end;;
diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/word_lib.ML
--- a/src/HOL/Library/Tools/word_lib.ML	Sun Mar 30 11:21:34 2025 +0200
+++ b/src/HOL/Library/Tools/word_lib.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -35,7 +35,7 @@
   then Type (\<^type_name>\<open>Numeral_Type.bit0\<close>, [T])
   else Type (\<^type_name>\<open>Numeral_Type.bit1\<close>, [T])
 
-fun mk_binT size = 
+fun mk_binT size =
   if size = 0 then \<^typ>\<open>Numeral_Type.num0\<close>
   else if size = 1 then \<^typ>\<open>Numeral_Type.num1\<close>
   else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
diff -r 23df00d48d6f -r 3f875966c3e1 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Mar 30 11:21:34 2025 +0200
+++ b/src/Tools/Code/code_target.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -652,7 +652,16 @@
 
 (* 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) =
@@ -662,23 +671,26 @@
     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)))
+        (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 ctxt;
+fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms I ctxt;
 
-fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms 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 *)
 
@@ -731,6 +743,9 @@
   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) =
@@ -763,7 +778,7 @@
   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 _ =