# HG changeset patch
# User wenzelm
# Date 1656684190 -7200
# Node ID bb048086468a6328c946b19771891e911bb71d81
# Parent  a7e0129b8b2d3093c11a4ab5899c8d9011af3c74
discontinued Isabelle tools implemented as .scala scripts;

diff -r a7e0129b8b2d -r bb048086468a NEWS
--- a/NEWS	Fri Jul 01 11:44:06 2022 +0200
+++ b/NEWS	Fri Jul 01 16:03:10 2022 +0200
@@ -195,6 +195,13 @@
 Isabelle repository: a regular download of the distribution will not
 work!
 
+* External Isabelle tools implemented as .scala scripts are no longer
+supported. INCOMPATIBILITY, instead provide a proper Isabelle/Scala
+module with etc/build.props and "services" for a suitable class instance
+of isabelle.Isabelle_Scala_Tools. For example, see
+$ISABELLE_HOME/etc/build.props and its isabelle.Tools, which defines the
+standard Isabelle tools.
+
 
 
 New in Isabelle2021-1 (December 2021)
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 ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the content needs to define
-      some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. 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>\<open>List[String]\<close>.
+    notation). It is invoked as stand-alone program with the command-line
+    arguments provided as \<^verbatim>\<open>argv\<close> array.
 
-      \<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as
-      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>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}).
+    \<^enum> An internal tool that is declared via class
+    \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close> and registered via
+    \<^verbatim>\<open>services\<close> in \<^path>\<open>etc/build.props\<close>. 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.
diff -r a7e0129b8b2d -r bb048086468a src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Jul 01 11:44:06 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Fri Jul 01 16:03:10 2022 +0200
@@ -1,6 +1,5 @@
 /*  Title:      Pure/System/isabelle_tool.scala
     Author:     Makarius
-    Author:     Lars Hupel
 
 Isabelle system tools: external executables or internal Scala functions.
 */
@@ -13,55 +12,15 @@
 
 
 object Isabelle_Tool {
-  /* Scala source tools */
-
-  abstract class Body extends Function[List[String], Unit]
-
-  private def compile(path: Path): Body = {
-    def err(msg: String): Nothing =
-      cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
-
-    val source = File.read(path)
-
-    val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
-    val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
-
-    try {
-      val tree = tool_box.parse(source)
-      val module =
-        try { tree.asInstanceOf[universe.ModuleDef] }
-        catch {
-          case _: java.lang.ClassCastException =>
-            err("Source does not describe a module (Scala object)")
-        }
-      tool_box.compile(universe.Ident(tool_box.define(module)))() match {
-        case body: Body => body
-        case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
-      }
-    }
-    catch {
-      case e: ToolBoxError =>
-        if (tool_box.frontEnd.hasErrors) {
-          val infos = tool_box.frontEnd.infos.toList
-          val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
-          err(msgs.mkString("\n"))
-        }
-        else
-          err(e.toString)
-    }
-  }
-
-
   /* external tools */
 
   private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
 
-  private def is_external(dir: Path, file_name: String): Boolean = {
-    val file = (dir + Path.explode(file_name)).file
+  private def is_external(dir: Path, name: String): Boolean = {
+    val file = (dir + Path.explode(name)).file
     try {
-      file.isFile && file.canRead &&
-        (file_name.endsWith(".scala") || file.canExecute) &&
-        !file_name.endsWith("~") && !file_name.endsWith(".orig")
+      file.isFile && file.canRead && file.canExecute &&
+        !name.endsWith("~") && !name.endsWith(".orig")
     }
     catch { case _: SecurityException => false }
   }
@@ -69,8 +28,6 @@
   private def find_external(name: String): Option[List[String] => Unit] =
     dirs().collectFirst(
       {
-        case dir if is_external(dir, name + ".scala") =>
-          compile(dir + Path.explode(name + ".scala"))
         case dir if is_external(dir, name) =>
           { (args: List[String]) =>
             val tool = dir + Path.explode(name)
@@ -116,12 +73,8 @@
   def external_tools(): List[External] = {
     for {
       dir <- dirs() if dir.is_dir
-      file_name <- File.read_dir(dir) if is_external(dir, file_name)
-    } yield {
-      val path = dir + Path.explode(file_name)
-      val name = Library.perhaps_unsuffix(".scala", file_name)
-      External(name, path)
-    }
+      name <- File.read_dir(dir) if is_external(dir, name)
+    } yield External(name, dir + Path.explode(name))
   }
 
   def isabelle_tools(): List[Entry] =