# HG changeset patch
# User wenzelm
# Date 1376686636 -7200
# Node ID 4c297ee47c28ca475ed612d62ab2b26d107c089f
# Parent  be27b6be8027e1fc52dda495e5352ba928b021f1
check_tool wrt. official ISABELLE_TOOLS;
added Path.split (cf. Scala version);

diff -r be27b6be8027 -r 4c297ee47c28 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Fri Aug 16 22:39:31 2013 +0200
+++ b/src/Doc/antiquote_setup.ML	Fri Aug 16 22:57:16 2013 +0200
@@ -150,13 +150,11 @@
 
 fun check_tool (name, pos) =
   let
-    (* FIXME ISABELLE_TOOLS !? *)
-    val dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"];
     fun tool dir =
       let val path = Path.append dir (Path.basic name)
       in if File.exists path then SOME path else NONE end;
   in
-    (case get_first tool dirs of
+    (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
       NONE => false
     | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
   end;
diff -r be27b6be8027 -r 4c297ee47c28 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Aug 16 22:39:31 2013 +0200
+++ b/src/Pure/General/path.ML	Fri Aug 16 22:57:16 2013 +0200
@@ -22,6 +22,7 @@
   val make: string list -> T
   val implode: T -> string
   val explode: string -> T
+  val split: string -> T list
   val pretty: T -> Pretty.T
   val print: T -> string
   val dir: T -> T
@@ -149,6 +150,10 @@
 
   in Path (norm (rev elems @ roots)) end;
 
+fun split str =
+  space_explode ":" str
+  |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
+
 
 (* print *)