# HG changeset patch
# User wenzelm
# Date 1117963881 -7200
# Node ID f3d913abf7e5ceb8499179c7e3b18d282b61e496
# Parent  98337d5acd0eea128d346a795701129354fbb563
File.shell_path;

diff -r 98337d5acd0e -r f3d913abf7e5 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 05 11:31:20 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 05 11:31:21 2005 +0200
@@ -503,7 +503,7 @@
       else mucke_home ^ "/mucke";
     val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
     val _ = File.write mucke_input_file s;
-    val result = execute (mucke ^ " -nb -res " ^ (File.quote_sysify_path mucke_input_file));
+    val result = execute (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
   in
     if not (!trace_mc) then (File.rm mucke_input_file) else (); 
     result
diff -r 98337d5acd0e -r f3d913abf7e5 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sun Jun 05 11:31:20 2005 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Sun Jun 05 11:31:21 2005 +0200
@@ -71,8 +71,8 @@
       val svc_output_file = File.tmp_path (Path.basic "SVM_out");
       val _ = (File.write svc_input_file svc_input;
 	       execute (check_valid ^ " -dump-result " ^ 
-			File.quote_sysify_path svc_output_file ^
-			" " ^ File.quote_sysify_path svc_input_file ^ 
+			File.shell_path svc_output_file ^
+			" " ^ File.shell_path svc_input_file ^ 
 			">/dev/null 2>&1"))
       val svc_output =
         (case Library.try File.read svc_output_file of
diff -r 98337d5acd0e -r f3d913abf7e5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Jun 05 11:31:20 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Jun 05 11:31:21 2005 +0200
@@ -188,12 +188,12 @@
 (* present draft files *)
 
 fun display_drafts files = Toplevel.imperative (fn () =>
-  let val outfile = File.quote_sysify_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
-  in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
+  let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
+  in File.isatool ("display -c " ^ outfile ^ " &"); () end);
 
 fun print_drafts files = Toplevel.imperative (fn () =>
-  let val outfile = File.quote_sysify_path (Present.drafts "ps" files)
-  in system ("\"$ISATOOL\" print -c " ^ outfile); () end);
+  let val outfile = File.shell_path (Present.drafts "ps" files)
+  in File.isatool ("print -c " ^ outfile); () end);
 
 
 (* pretty_setmargin *)