File.quote_sysify_path;
authorwenzelm
Mon Jun 21 16:39:09 2004 +0200 (2004-06-21)
changeset 14982ff1c919f4982
parent 14981 e73f8140af78
child 14983 2b5e9b80a8e5
File.quote_sysify_path;
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 21 10:25:57 2004 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 21 16:39:09 2004 +0200
     1.3 @@ -500,7 +500,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.sysify_path mucke_input_file));
     1.8 +    val result = execute (mucke ^ " -nb -res " ^ (File.quote_sysify_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	Mon Jun 21 10:25:57 2004 +0200
     2.2 +++ b/src/HOL/ex/svc_funcs.ML	Mon Jun 21 16:39:09 2004 +0200
     2.3 @@ -71,9 +71,9 @@
     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.sysify_path svc_output_file ^
     2.8 -			" " ^ File.sysify_path svc_input_file ^ 
     2.9 -			"> /dev/null 2>&1"))
    2.10 +			File.quote_sysify_path svc_output_file ^
    2.11 +			" " ^ File.quote_sysify_path svc_input_file ^ 
    2.12 +			">/dev/null 2>&1"))
    2.13        val svc_output =
    2.14          (case Library.try File.read svc_output_file of
    2.15            Some out => out