src/Pure/Thy/thm_deps.ML
changeset 16268 d978482479d3
parent 15570 8d8c70b41bab
child 16894 40f80823b451
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Sun Jun 05 11:31:31 2005 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sun Jun 05 11:31:32 2005 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4                      (case ThyInfo.lookup_theory x of
     1.5                        SOME thy =>
     1.6                          let val name = #name (Present.get_info thy)
     1.7 -                        in if name = "" then [] else [name] end 
     1.8 +                        in if name = "" then [] else [name] end
     1.9                      | NONE => [])
    1.10                   | _ => ["global"]);
    1.11              in
    1.12 @@ -72,7 +72,7 @@
    1.13        map Thm.proof_of thms))));
    1.14      val path = File.tmp_path (Path.unpack "theorems.graph");
    1.15      val _ = Present.write_graph gra path;
    1.16 -    val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    1.17 +    val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &");
    1.18    in () end;
    1.19  
    1.20  end;