check_tool wrt. official ISABELLE_TOOLS;
added Path.split (cf. Scala version);
--- 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 *)