diff -r a7e0129b8b2d -r bb048086468a src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Fri Jul 01 11:44:06 2022 +0200 +++ b/src/Doc/System/Environment.thy Fri Jul 01 16:03:10 2022 +0200 @@ -284,25 +284,13 @@ \<^enum> An external tool found on the directories listed in the @{setting ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX - notation). - - \<^enum> If a file ``\tool\\<^verbatim>\.scala\'' is found, the content needs to define - some object that extends the class \<^verbatim>\Isabelle_Tool.Body\. The Scala - compiler is invoked on the spot (which may take some time), and the body - function is run with the command-line arguments as \<^verbatim>\List[String]\. + notation). It is invoked as stand-alone program with the command-line + arguments provided as \<^verbatim>\argv\ array. - \<^enum> If an executable file ``\tool\'' is found, it is invoked as - stand-alone program with the command-line arguments provided as \<^verbatim>\argv\ - array. - - \<^enum> An internal tool that is registered in \<^verbatim>\etc/settings\ via the shell - function \<^bash_function>\isabelle_scala_service\, referring to a - suitable instance of class \<^scala_type>\isabelle.Isabelle_Scala_Tools\. - This is the preferred approach for non-trivial systems programming in - Isabelle/Scala: instead of adhoc interpretation of \<^verbatim>\scala\ scripts, - which is somewhat slow and only type-checked at runtime, there are - properly compiled \<^verbatim>\jar\ modules (see also the shell function - \<^bash_function>\classpath\ in \secref{sec:scala}). + \<^enum> An internal tool that is declared via class + \<^scala_type>\isabelle.Isabelle_Scala_Tools\ and registered via + \<^verbatim>\services\ in \<^path>\etc/build.props\. See \secref{sec:scala-build} for + more details. There are also various administrative tools that are available from a bare repository clone of Isabelle, but not in regular distributions.