check_tool wrt. official ISABELLE_TOOLS;
authorwenzelm
Fri, 16 Aug 2013 22:57:16 +0200
changeset 53045 4c297ee47c28
parent 53044 be27b6be8027
child 53046 cba2ddfb30c4
check_tool wrt. official ISABELLE_TOOLS; added Path.split (cf. Scala version);
src/Doc/antiquote_setup.ML
src/Pure/General/path.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;
--- 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 *)