add find_facts_index command to use within Isabelle/Scala;
authorFabian Huch <huch@in.tum.de>
Thu, 16 Jan 2025 19:00:29 +0100
changeset 81880 b1f6e80cfff9
parent 81879 05c0778360d3
child 81881 f23fc3d21873
add find_facts_index command to use within Isabelle/Scala;
src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Thu Jan 16 18:37:23 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Thu Jan 16 19:00:29 2025 +0100
@@ -577,6 +577,21 @@
       } yield block)
   }
 
+  def find_facts_index_command(
+    sessions: List[String],
+    ssh: SSH.System = SSH.Local,
+    isabelle_home: Path = Path.current,
+    options: List[Options.Spec] = Nil,
+    dirs: List[Path] = Nil,
+    clean: Boolean = false
+  ): String = {
+    ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " find_facts_index" +
+      dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
+      if_proper(clean, " -c") +
+      Options.Spec.bash_strings(options, bg = true) +
+      sessions.map(session => " " + session).mkString
+  }
+  
   def find_facts_index(
     options: Options,
     sessions: List[String],