--- 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)
--- 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.
--- 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] =