File.isatool, File.shell_path;
authorwenzelm
Sun, 05 Jun 2005 11:31:32 +0200
changeset 16268 d978482479d3
parent 16267 0773b17922d8
child 16269 2c05a7f662a3
File.isatool, File.shell_path;
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;