# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737050429 -3600
# Node ID b1f6e80cfff9c60b25347a6134af37c850c1b2a5
# Parent  05c0778360d3908cbcb1111508c1039fcfd9cab0
add find_facts_index command to use within Isabelle/Scala;

diff -r 05c0778360d3 -r b1f6e80cfff9 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],