more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);

--- a/NEWS	Sat Sep 10 16:57:18 2022 +0200
+++ b/NEWS	Sat Sep 10 19:37:33 2022 +0200
@@ -328,6 +328,14 @@
 Note that printing intermediate states may cause considerable slowdown
 in building a session.
 
+* Session ROOT entries support 'export_classpath' to augment the
+Java/Scala name space for tools that allow dynamic loading of service
+classes within a session context. A notable example is document
+preparation, which works via the class isabelle.Document_Build.Engine
+and is configured by the corresponding system option "document_build".
+The Isabelle/Isar command 'scala_build_generated_files' helps to produce
+a suitable .jar module for inclusion via 'export_classpath'.
+
 
 
 New in Isabelle2021-1 (December 2021)

--- a/src/Doc/Isar_Ref/Spec.thy	Sat Sep 10 16:57:18 2022 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Sep 10 19:37:33 2022 +0200
@@ -1327,8 +1327,9 @@
   corresponding @{path build.props} file is expected directly in the toplevel
   directory, instead of @{path "etc/build.props"} for Isabelle system
   components. These properties need to specify sources, resources, services
-  etc. as usual. The resulting \<^verbatim>\<open>jar\<close> module becomes an export artifact of the
-  session database.
+  etc. as usual. The resulting JAR module becomes an export artefact of the
+  session database, with a name of the form
+  ``\<open>theory\<close>\<^verbatim>\<open>:classpath/\<close>\<open>module\<close>\<^verbatim>\<open>.jar\<close>''.
 
   \<^descr> \<^theory_text>\<open>compile_generated_files paths (in thy) where compile_body\<close> retrieves
   named generated files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into

--- a/src/Doc/System/Sessions.thy	Sat Sep 10 16:57:18 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Sat Sep 10 19:37:33 2022 +0200
@@ -61,7 +61,7 @@
       (@{syntax system_name} '+')? description? options? \<newline>
       sessions? directories? (theories*) \<newline>
       (document_theories?) (document_files*) \<newline>
-      (export_files*)
+      (export_files*) (export_classpath?)
     ;
     groups: '(' (@{syntax name} +) ')'
     ;
@@ -89,6 +89,8 @@
     ;
     export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline>
       (@{syntax embedded}+)
+    ;
+    export_classpath: @'export_classpath' (@{syntax embedded}*)
   \<close>
 
   \<^descr> \isakeyword{chapter{\isacharunderscorekeyword}definition}~\<open>A (groups)\<close>
@@ -182,6 +184,15 @@
   0) specifies the prefix of elements that should be removed from each name:
   it allows to reduce the resulting directory hierarchy at the danger of
   overwriting files due to loss of uniqueness.
+
+  \<^descr> \isakeyword{export_classpath}~\<open>patterns\<close> specifies export artifacts that
+  should be included into the local Java/Scala classpath of this session
+  context. This is only relevant for tools that allow dynamic loading of
+  service classes (\secref{sec:scala-build}), while most other Isabelle/Scala
+  tools require global configuration during system startup. An empty list of
+  \<open>patterns\<close> defaults to \<^verbatim>\<open>"*:classpath/*.jar"\<close>, which fits to the naming
+  convention of JAR modules produced by the Isabelle/Isar command
+  \<^theory_text>\<open>scala_build_generated_files\<close> @{cite "isabelle-isar-ref"}.
 \<close>