# HG changeset patch
# User wenzelm
# Date 1246116888 -7200
# Node ID f698f76a371336a50dc8ec476449d70757184015
# Parent  9b34b1449cb7f060a46c0ee15c1d0bfdda6994a0
builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);

diff -r 9b34b1449cb7 -r f698f76a3713 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Jun 27 10:26:42 2009 +0200
+++ b/src/Pure/General/file.ML	Sat Jun 27 17:34:48 2009 +0200
@@ -12,7 +12,7 @@
   val pwd: unit -> Path.T
   val full_path: Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
-  val isabelle_tool: string -> int
+  val isabelle_tool: string -> string -> int
   val system_command: string -> unit
   eqtype ident
   val rep_ident: ident -> string
@@ -65,7 +65,17 @@
 
 (* system commands *)
 
-fun isabelle_tool cmd = system ("\"$ISABELLE_TOOL\" " ^ cmd);
+fun isabelle_tool name args =
+  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
+      let val path = dir ^ "/" ^ name in
+        if can OS.FileSys.modTime path andalso
+          not (OS.FileSys.isDir path) andalso
+          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
+        then SOME path
+        else NONE
+      end handle OS.SysErr _ => NONE) of
+    SOME path => system (shell_quote path ^ " " ^ args)
+  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
 
 fun system_command cmd =
   if system cmd <> 0 then error ("System command failed: " ^ cmd)
diff -r 9b34b1449cb7 -r f698f76a3713 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 27 10:26:42 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 27 17:34:48 2009 +0200
@@ -237,10 +237,18 @@
     Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
   }
 
-  def isabelle_tool(args: String*): (String, Int) =
+  def isabelle_tool(name: String, args: String*): (String, Int) =
   {
-    val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
-    Isabelle_System.process_output(proc)
+    getenv_strict("ISABELLE_TOOLS").split(":").find(dir => {
+      val file = platform_file(dir + "/" + name)
+      try { file.isFile && file.canRead && file.canExecute }
+      catch { case _: SecurityException => false }
+    }) match {
+      case Some(dir) =>
+        val proc = execute(true, (List(platform_path(dir + "/" + name)) ++ args): _*)
+        Isabelle_System.process_output(proc)
+      case None => ("Unknown Isabelle tool: " + name, 2)
+    }
   }