# HG changeset patch
# User wenzelm
# Date 1657633377 -7200
# Node ID aa89255b704c43309d9e58c1cadad7561ea9cd9d
# Parent  58b1617466458234ba24e3dc5dd5d4a61e913e1c
support for classpath artifacts within session structure:

diff -r 58b161746645 -r aa89255b704c src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Pure.thy	Tue Jul 12 15:42:57 2022 +0200
@@ -24,6 +24,7 @@
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
   and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
+  and "export_classpath"
   and "scala_build_component" "scala_build_directory" :: diag
   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
diff -r 58b161746645 -r aa89255b704c src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue Jul 12 15:42:57 2022 +0200
@@ -121,10 +121,12 @@
     db_context: Sessions.Database_Context,
     progress: Progress = new Progress
   ): Context = {
-    val info = deps.sessions_structure(session)
+    val structure = deps.sessions_structure
+    val info = structure(session)
     val base = deps(session)
     val hierarchy = deps.sessions_structure.build_hierarchy(session)
-    new Context(info, base, hierarchy, db_context, progress)
+    val classpath = db_context.get_classpath(structure, session)
+    new Context(info, base, hierarchy, db_context, classpath, progress)
   }
 
   final class Context private[Document_Build](
@@ -132,6 +134,7 @@
     base: Sessions.Base,
     hierarchy: List[String],
     db_context: Sessions.Database_Context,
+    val classpath: List[File.Content_Bytes],
     val progress: Progress = new Progress
   ) {
     /* session info */
diff -r 58b161746645 -r aa89255b704c src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Thy/sessions.ML	Tue Jul 12 15:42:57 2022 +0200
@@ -41,6 +41,9 @@
   Parse.$$$ "export_files" |--
     Parse.!!! (Scan.optional in_path (Input.string "export") -- prune -- Scan.repeat1 Parse.embedded);
 
+val export_classpath =
+  Parse.$$$ "export_classpath" |-- Scan.repeat Parse.embedded;
+
 fun path_source source path =
   Input.source (Input.is_delimited source) (Path.implode path) (Input.range_of source);
 
@@ -60,10 +63,11 @@
       Scan.repeat theories --
       Scan.optional document_theories [] --
       Scan.repeat document_files --
-      Scan.repeat export_files))
+      Scan.repeat export_files --
+      Scan.optional export_classpath []))
   >> (fn (((((session, _), _), dir),
-          (((((((((parent, descr), options), sessions), directories), theories),
-            document_theories), document_files), export_files)))) =>
+          ((((((((((parent, descr), options), sessions), directories), theories),
+            document_theories), document_files), export_files), _)))) =>
     Toplevel.keep (fn state =>
       let
         val ctxt = Toplevel.context_of state;
diff -r 58b161746645 -r aa89255b704c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Jul 12 14:40:41 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Jul 12 15:42:57 2022 +0200
@@ -429,7 +429,8 @@
                   theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
                   document_theories = Nil,
                   document_files = Nil,
-                  export_files = Nil))))
+                  export_files = Nil,
+                  export_classpath = Nil))))
         }
       }
       else (session, Nil)
@@ -466,6 +467,7 @@
     document_theories: List[(String, Position.T)],
     document_files: List[(Path, Path)],
     export_files: List[(Path, Int, List[String])],
+    export_classpath: List[String],
     meta_digest: SHA1.Digest
   ) {
     def chapter_session: String = chapter + "/" + name
@@ -599,7 +601,7 @@
       Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
         entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, entry.document_theories, document_files,
-        export_files, meta_digest)
+        export_files, entry.export_classpath, meta_digest)
     }
     catch {
       case ERROR(msg) =>
@@ -860,6 +862,7 @@
   private val DOCUMENT_THEORIES = "document_theories"
   private val DOCUMENT_FILES = "document_files"
   private val EXPORT_FILES = "export_files"
+  private val EXPORT_CLASSPATH = "export_classpath"
 
   val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
@@ -873,7 +876,8 @@
       (THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
-      (EXPORT_FILES, Keyword.QUASI_COMMAND)
+      (EXPORT_FILES, Keyword.QUASI_COMMAND) +
+      (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
 
   abstract class Entry
   sealed case class Chapter(name: String) extends Entry
@@ -890,7 +894,8 @@
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_theories: List[(String, Position.T)],
     document_files: List[(String, String)],
-    export_files: List[(String, Int, List[String])]
+    export_files: List[(String, Int, List[String])],
+    export_classpath: List[String]
   ) extends Entry {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
@@ -934,6 +939,10 @@
         $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
           { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
+      val export_classpath =
+        $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^
+          { case _ ~ x => x }
+
       command(SESSION) ~!
         (position(session_name) ~
           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
@@ -947,9 +956,10 @@
               rep(theories) ~
               (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~
               (rep(document_files) ^^ (x => x.flatten)) ~
-              rep(export_files)))) ^^
-        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l))) =>
-            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l) }
+              rep(export_files) ~
+              opt(export_classpath)))) ^^
+        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l ~ m))) =>
+            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l, m.getOrElse(Nil)) }
     }
 
     def parse_root(path: Path): List[Entry] = {
@@ -1236,6 +1246,26 @@
       read_export(session_hierarchy, theory_name, name) getOrElse
         Export.empty_entry(theory_name, name)
 
+    def get_classpath(structure: Structure, session: String): List[File.Content_Bytes] =
+    {
+      (for {
+        name <- structure.build_requirements(List(session))
+        patterns = structure(name).export_classpath if patterns.nonEmpty
+      } yield {
+        input_database(name)((db, _) =>
+          db.transaction {
+            val matcher = Export.make_matcher(patterns)
+            val res =
+              for {
+                entry_name <- Export.read_entry_names(db, name) if matcher(entry_name)
+                entry <- entry_name.read(db, store.cache)
+              } yield File.Content(Path.make(entry.entry_name.elements()), entry.uncompressed)
+            Some(res)
+          }
+        ).getOrElse(Nil)
+      }).flatten
+    }
+
     override def toString: String = {
       val s =
         database_server match {