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