# HG changeset patch
# User wenzelm
# Date 1117963892 -7200
# Node ID d978482479d34eb5c4987cc4f7b57e18c3c86947
# Parent  0773b17922d8a569803c1f029428f90307b051b8
File.isatool, File.shell_path;

diff -r 0773b17922d8 -r d978482479d3 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sun Jun 05 11:31:31 2005 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sun Jun 05 11:31:32 2005 +0200
@@ -49,7 +49,7 @@
                     (case ThyInfo.lookup_theory x of
                       SOME thy =>
                         let val name = #name (Present.get_info thy)
-                        in if name = "" then [] else [name] end 
+                        in if name = "" then [] else [name] end
                     | NONE => [])
                  | _ => ["global"]);
             in
@@ -72,7 +72,7 @@
       map Thm.proof_of thms))));
     val path = File.tmp_path (Path.unpack "theorems.graph");
     val _ = Present.write_graph gra path;
-    val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
+    val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &");
   in () end;
 
 end;