From 5471d873a9320a2ed28a46402928c7542cf5e784 Mon Sep 17 00:00:00 2001
From: Makarius <makarius@sketis.net>
Date: Sun, 4 Dec 2022 19:13:08 +0100
Subject: [PATCH] Isabelle/Scala module within session context supports
 document_build = "dof" without component setup

---
 .woodpecker/build.yml |  1 +
 src/DOF/Isa_DOF.thy   | 31 +++++++++++++++++++++++++++++++
 src/tests/ROOT        |  3 ++-
 3 files changed, 34 insertions(+), 1 deletion(-)

diff --git a/.woodpecker/build.yml b/.woodpecker/build.yml
index 26637b3..82fb642 100644
--- a/.woodpecker/build.yml
+++ b/.woodpecker/build.yml
@@ -7,6 +7,7 @@ pipeline:
       - export `isabelle getenv ISABELLE_HOME_USER`
       - mkdir -p $ISABELLE_HOME_USER/etc
       - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
+      - isabelle build -D . -o browser_info
       - isabelle components -u .
       - isabelle build -D . -o browser_info
       - isabelle dof_mkroot DOF_test
diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index eda9b4a..e758133 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -3022,6 +3022,37 @@ define_template "../document-templates/root-scrreprt-modern.tex"
 define_template "../document-templates/root-scrreprt.tex"
 define_template "../document-templates/root-svjour3-UNSUPPORTED.tex"
 
+
+section \<open>Isabelle/Scala module within session context\<close>
+
+external_file "../../etc/build.props"
+external_file "../scala/dof_document_build.scala"
+external_file "../scala/dof_mkroot.scala"
+external_file "../scala/dof.scala"
+external_file "../scala/dof_tools.scala"
+
+ML_command \<open>
+  Isabelle_System.with_tmp_dir "scala_build" (fn dir =>
+    let
+      val _ = Isabelle_System.copy_file (\<^master_dir> + Path.explode "../../etc/build.props") dir;
+      val scala_dir = \<^master_dir> + Path.explode "../scala";
+      val dest = Isabelle_System.make_directory (dir + Path.explode "src/scala");
+      val _ =
+        List.app (fn name => Isabelle_System.copy_file (scala_dir + Path.basic name) dest)
+          ["dof_document_build.scala",
+           "dof_mkroot.scala",
+           "dof.scala",
+           "dof_tools.scala"];
+      val [jar_name, jar_bytes, output] =
+        \<^scala>\<open>scala_build\<close> [Bytes.string (Isabelle_System.absolute_path dir)];
+      val _ = writeln (Bytes.content output);
+    in
+      Export.export \<^theory>
+        (Path.explode_binding0 (Bytes.content jar_name))
+        (Bytes.contents_blob jar_bytes)
+    end)
+\<close>
+
 (*
 ML\<open>
    Pretty.text;
diff --git a/src/tests/ROOT b/src/tests/ROOT
index 6a97b0b..39f6ee7 100644
--- a/src/tests/ROOT
+++ b/src/tests/ROOT
@@ -7,6 +7,7 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
     "TermAntiquotations"
     "Attributes"
     "Evaluation"
-    "Isabelle2022"
     "High_Level_Syntax_Invariants"
     "Ontology_Matching_Example"
+  theories [condition = ISABELLE_DOF_HOME]
+    "Isabelle2022"