File.shell_path;
authorwenzelm
Sun Jun 05 11:31:21 2005 +0200 (2005-06-05)
changeset 16258f3d913abf7e5
parent 16257 98337d5acd0e
child 16259 aed1a8ae4b23
File.shell_path;
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/ex/svc_funcs.ML
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 05 11:31:20 2005 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sun Jun 05 11:31:21 2005 +0200
     1.3 @@ -503,7 +503,7 @@
     1.4        else mucke_home ^ "/mucke";
     1.5      val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
     1.6      val _ = File.write mucke_input_file s;
     1.7 -    val result = execute (mucke ^ " -nb -res " ^ (File.quote_sysify_path mucke_input_file));
     1.8 +    val result = execute (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
     1.9    in
    1.10      if not (!trace_mc) then (File.rm mucke_input_file) else (); 
    1.11      result
     2.1 --- a/src/HOL/ex/svc_funcs.ML	Sun Jun 05 11:31:20 2005 +0200
     2.2 +++ b/src/HOL/ex/svc_funcs.ML	Sun Jun 05 11:31:21 2005 +0200
     2.3 @@ -71,8 +71,8 @@
     2.4        val svc_output_file = File.tmp_path (Path.basic "SVM_out");
     2.5        val _ = (File.write svc_input_file svc_input;
     2.6  	       execute (check_valid ^ " -dump-result " ^ 
     2.7 -			File.quote_sysify_path svc_output_file ^
     2.8 -			" " ^ File.quote_sysify_path svc_input_file ^ 
     2.9 +			File.shell_path svc_output_file ^
    2.10 +			" " ^ File.shell_path svc_input_file ^ 
    2.11  			">/dev/null 2>&1"))
    2.12        val svc_output =
    2.13          (case Library.try File.read svc_output_file of
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jun 05 11:31:20 2005 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jun 05 11:31:21 2005 +0200
     3.3 @@ -188,12 +188,12 @@
     3.4  (* present draft files *)
     3.5  
     3.6  fun display_drafts files = Toplevel.imperative (fn () =>
     3.7 -  let val outfile = File.quote_sysify_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
     3.8 -  in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
     3.9 +  let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
    3.10 +  in File.isatool ("display -c " ^ outfile ^ " &"); () end);
    3.11  
    3.12  fun print_drafts files = Toplevel.imperative (fn () =>
    3.13 -  let val outfile = File.quote_sysify_path (Present.drafts "ps" files)
    3.14 -  in system ("\"$ISATOOL\" print -c " ^ outfile); () end);
    3.15 +  let val outfile = File.shell_path (Present.drafts "ps" files)
    3.16 +  in File.isatool ("print -c " ^ outfile); () end);
    3.17  
    3.18  
    3.19  (* pretty_setmargin *)