# HG changeset patch
# User wenzelm
# Date 1737292993 -3600
# Node ID 61b7111220616c3a6f507a54a18d48b4e984cfae
# Parent  02b4ae06974d66a09314fba87e1ef6c4efbc3ecb
allow to load additional HOL Light files, after "hol.ml";

diff -r 02b4ae06974d -r 61b711122061 src/HOL/Import/patches/patch1
--- a/src/HOL/Import/patches/patch1	Sat Jan 18 23:46:46 2025 +0100
+++ b/src/HOL/Import/patches/patch1	Sun Jan 19 14:23:13 2025 +0100
@@ -18,14 +18,16 @@
 +dump_theorems ();;
 --- hol-light/stage1.ml	1970-01-01 01:00:00.000000000 +0100
 +++ hol-light-patched/stage1.ml	2025-01-18 11:12:11.185279392 +0100
-@@ -0,0 +1,4 @@
+@@ -0,0 +1,5 @@
 +#use "hol.ml";;
++(*LOAD MORE*)
 +#use "update_database.ml";;
 +#use "statements.ml";;
 +exit 0;;
 --- hol-light/stage2.ml	1970-01-01 01:00:00.000000000 +0100
 +++ hol-light-patched/stage2.ml	2025-01-18 11:12:11.384276293 +0100
-@@ -0,0 +1,3 @@
+@@ -0,0 +1,4 @@
 +#use "hol.ml";;
++(*LOAD MORE*)
 +stop_recording ();;
 +exit 0;;
diff -r 02b4ae06974d -r 61b711122061 src/Pure/Admin/component_hol_light.scala
--- a/src/Pure/Admin/component_hol_light.scala	Sat Jan 18 23:46:46 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala	Sun Jan 19 14:23:13 2025 +0100
@@ -20,6 +20,7 @@
     only_offline: Boolean = false,
     progress: Progress = new Progress,
     target_dir: Path = Path.current,
+    load_more: List[Path] = Nil,
     hol_light_url: String = default_hol_light_url,
     hol_light_rev: String = default_hol_light_rev
   ): Unit = {
@@ -118,6 +119,7 @@
         /* clone repository */
 
         val hol_light_dir = tmp_dir + Path.basic("hol-light")
+
         Isabelle_System.git_clone(hol_light_url, hol_light_dir, checkout = hol_light_rev,
           progress = progress)
 
@@ -131,6 +133,15 @@
 
         for (n <- List(1, 2)) Isabelle_System.copy_file(patch(n, source = true), patch(n))
 
+        if (load_more.nonEmpty) {
+          val bad = load_more.filter(path => !(hol_light_dir + path).is_file)
+          if (bad.nonEmpty) error("Bad HOL Light files: " + bad.mkString(", "))
+
+          val more = load_more.map(path => "needs " + path + ";; ").mkString("+", "", "")
+          File.change_lines(patch(1), strict = true)(_.map(line =>
+            if (line == "+(*LOAD MORE*)") more else line))
+        }
+
 
         /* export stages */
 
@@ -176,6 +187,7 @@
       Scala_Project.here,
       { args =>
         var target_dir = Path.current
+        var load_more = List.empty[Path]
         var only_offline = false
         var hol_light_url = default_hol_light_url
         var hol_light_rev = default_hol_light_rev
@@ -186,6 +198,7 @@
 
   Options are:
     -D DIR       target directory (default ".")
+    -L PATH      load additional HOL Light files, after "hol.ml"
     -O           only build the "offline" tool
     -U URL       git URL for original HOL Light repository, default:
                  """ + default_hol_light_url + """
@@ -193,9 +206,13 @@
                     default_hol_light_rev + """)
     -v           verbose
 
-  Build Isabelle component for HOL Light import.
+  Build Isabelle component for HOL Light import. For example:
+
+    isabelle component_hol_light_import -L Logic/make.ml
+    isabelle component_hol_light_import -L 100/thales.ml -L 100/ceva.ml
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
+          "L:" -> (arg => load_more = load_more ::: List(Path.explode(arg))),
           "O" -> (_ => only_offline = true),
           "U:" -> (arg => hol_light_url = arg),
           "r:" -> (arg => hol_light_rev = arg),
@@ -208,6 +225,6 @@
 
         build_hol_light_import(
           only_offline = only_offline, progress = progress, target_dir = target_dir,
-          hol_light_url = hol_light_url, hol_light_rev = hol_light_rev)
+          load_more = load_more, hol_light_url = hol_light_url, hol_light_rev = hol_light_rev)
       })
 }