# HG changeset patch
# User wenzelm
# Date 1599819439 -7200
# Node ID 3b17e7688dc6a6f095ec9cd7cb71e7dc2aa594e4
# Parent  a6587b40399d5f20aaa0134478faffe58c024ff2
updated documentation;

diff -r a6587b40399d -r 3b17e7688dc6 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Fri Sep 11 11:44:03 2020 +0200
+++ b/src/Doc/System/Environment.thy	Fri Sep 11 12:17:19 2020 +0200
@@ -308,13 +308,16 @@
       stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
       array.
 
-    \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
-    within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
-    entry-point for high-end tools implemented in Isabelle/Scala --- compiled
-    once when the Isabelle distribution is built. These tools are provided by
-    Isabelle/Pure and cannot be augmented in user-space.
+    \<^enum> An internal tool that is registered in \<^verbatim>\<open>etc/settings\<close> via the shell
+    function \<^bash_function>\<open>isabelle_scala_service\<close>, referring to a
+    suitable instance of class \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close>.
+    This is the preferred approach for non-trivial systems programming in
+    Isabelle/Scala: instead of adhoc interpretation of \<^verbatim>\<open>scala\<close> scripts,
+    which is somewhat slow and only type-checked at runtime, there are
+    properly compiled \<^verbatim>\<open>jar\<close> modules (see also the shell function
+    \<^bash_function>\<open>classpath\<close> in \secref{sec:scala}).
 
-  There are also some administrative tools that are available from a bare
+  There are also various administrative tools that are available from a bare
   repository clone of Isabelle, but not in regular distributions.
 \<close>
 
diff -r a6587b40399d -r 3b17e7688dc6 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Fri Sep 11 11:44:03 2020 +0200
+++ b/src/Doc/System/Scala.thy	Fri Sep 11 12:17:19 2020 +0200
@@ -4,7 +4,7 @@
 imports Base
 begin
 
-chapter \<open>Isabelle/Scala systems programming\<close>
+chapter \<open>Isabelle/Scala systems programming \label{sec:scala}\<close>
 
 text \<open>
   Isabelle/ML and Isabelle/Scala are the two main implementation languages of