check_tool wrt. official ISABELLE_TOOLS;
added Path.split (cf. Scala version);
1.1 --- a/src/Doc/antiquote_setup.ML Fri Aug 16 22:39:31 2013 +0200
1.2 +++ b/src/Doc/antiquote_setup.ML Fri Aug 16 22:57:16 2013 +0200
1.3 @@ -150,13 +150,11 @@
1.4
1.5 fun check_tool (name, pos) =
1.6 let
1.7 - (* FIXME ISABELLE_TOOLS !? *)
1.8 - val dirs = map Path.explode ["~~/lib/Tools", "~~/src/Tools/jEdit/lib/Tools"];
1.9 fun tool dir =
1.10 let val path = Path.append dir (Path.basic name)
1.11 in if File.exists path then SOME path else NONE end;
1.12 in
1.13 - (case get_first tool dirs of
1.14 + (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
1.15 NONE => false
1.16 | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
1.17 end;
2.1 --- a/src/Pure/General/path.ML Fri Aug 16 22:39:31 2013 +0200
2.2 +++ b/src/Pure/General/path.ML Fri Aug 16 22:57:16 2013 +0200
2.3 @@ -22,6 +22,7 @@
2.4 val make: string list -> T
2.5 val implode: T -> string
2.6 val explode: string -> T
2.7 + val split: string -> T list
2.8 val pretty: T -> Pretty.T
2.9 val print: T -> string
2.10 val dir: T -> T
2.11 @@ -149,6 +150,10 @@
2.12
2.13 in Path (norm (rev elems @ roots)) end;
2.14
2.15 +fun split str =
2.16 + space_explode ":" str
2.17 + |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
2.18 +
2.19
2.20 (* print *)
2.21