proper services for Setup_Tool --- avoid hardwired stuff;
authorwenzelm
Wed, 27 Mar 2024 12:50:37 +0100
changeset 80021 ba06861e91f9
parent 80020 b0a46cf73aa4
child 80022 77e605c66797
proper services for Setup_Tool --- avoid hardwired stuff;
etc/build.props
src/Pure/Admin/build_history.scala
src/Pure/System/other_isabelle.scala
src/Pure/System/setup_tool.scala
--- a/etc/build.props	Wed Mar 27 10:54:47 2024 +0100
+++ b/etc/build.props	Wed Mar 27 12:50:37 2024 +0100
@@ -197,6 +197,7 @@
   src/Pure/System/progress.scala \
   src/Pure/System/registry.scala \
   src/Pure/System/scala.scala \
+  src/Pure/System/setup_tool.scala \
   src/Pure/System/system_channel.scala \
   src/Pure/System/tty_loop.scala \
   src/Pure/Thy/document_build.scala \
@@ -333,7 +334,9 @@
   isabelle.Document_Build$LuaLaTeX_Engine \
   isabelle.Document_Build$PDFLaTeX_Engine \
   isabelle.CI_Builds \
+  isabelle.GHC_Setup \
   isabelle.ML_Statistics$Handler \
+  isabelle.OCaml_Setup \
   isabelle.Print_Operation$Handler \
   isabelle.Scala$Handler \
   isabelle.Scala_Functions \
--- a/src/Pure/Admin/build_history.scala	Wed Mar 27 10:54:47 2024 +0100
+++ b/src/Pure/Admin/build_history.scala	Wed Mar 27 12:50:37 2024 +0100
@@ -213,13 +213,7 @@
       if (first_build) {
         resolve_components()
         other_isabelle.scala_build(fresh = fresh, echo = verbose)
-
-        for {
-          tool <- List("ghc_setup", "ocaml_setup")
-          if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
-            (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
-        } other_isabelle.bash("bin/isabelle " + tool, echo = verbose)
-
+        Setup_Tool.init(other_isabelle, verbose = verbose)
         Isabelle_System.rm_tree(isabelle_base_log)
       }
 
--- a/src/Pure/System/other_isabelle.scala	Wed Mar 27 10:54:47 2024 +0100
+++ b/src/Pure/System/other_isabelle.scala	Wed Mar 27 12:50:37 2024 +0100
@@ -36,6 +36,8 @@
   ssh: SSH.System,
   progress: Progress
 ) {
+  other_isabelle =>
+
   override def toString: String = isabelle_home_url
 
 
@@ -173,6 +175,7 @@
       clean_archives = clean_archives,
       component_repository = component_repository)
     scala_build(fresh = fresh, echo = echo)
+    Setup_Tool.init(other_isabelle)
   }
 
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/setup_tool.scala	Wed Mar 27 12:50:37 2024 +0100
@@ -0,0 +1,37 @@
+/*  Title:      Pure/System/setup_tool.scala
+    Author:     Makarius
+
+Additional setup tools for other Isabelle distribution.
+*/
+
+package isabelle
+
+
+object Setup_Tool {
+  lazy val services: List[Setup_Tool] =
+    Isabelle_System.make_services(classOf[Setup_Tool])
+
+  def init(other_isabelle: Other_Isabelle, verbose: Boolean = false): Unit =
+    services.foreach(_.init(other_isabelle, verbose = verbose))
+}
+
+abstract class Setup_Tool(tool: String)
+extends Isabelle_System.Service {
+  override def toString: String = tool
+
+  val variable: String = "ISABELLE_" + Word.uppercase(tool)
+  val files: List[Path] = List(Path.explode("lib/Tools") + Path.basic(tool))
+
+  def test(other_isabelle: Other_Isabelle): Boolean =
+    other_isabelle.getenv(variable) == "true" &&
+    files.exists(p => (other_isabelle.isabelle_home + p).is_file)
+
+  def run(other_isabelle: Other_Isabelle, verbose: Boolean = false): Unit =
+    other_isabelle.bash("bin/isabelle " + Bash.string(tool), echo = verbose)
+
+  def init(other_isabelle: Other_Isabelle, verbose: Boolean = false): Unit =
+    if (test(other_isabelle)) run(other_isabelle, verbose = verbose)
+}
+
+class GHC_Setup extends Setup_Tool("ghc_setup")
+class OCaml_Setup extends Setup_Tool("ocaml_setup")