# HG changeset patch
# User blanchet
# Date 1265365493 -3600
# Node ID a886420664483951a08490f724991820dfd73076
# Parent  534005fff7fe8aeb17bafed03c8d9a67eeaf42ed
proper quoting of file paths when invoking Kodkodi from Nitpick

diff -r 534005fff7fe -r a88642066448 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Fri Feb 05 11:15:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Fri Feb 05 11:24:53 2010 +0100
@@ -1053,7 +1053,7 @@
           val outcome =
             let
               val code =
-                system ("cd " ^ temp_dir ^ ";\n" ^
+                system ("cd " ^ File.shell_quote temp_dir ^ ";\n" ^
                         "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
                         \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
                         \$JAVA_LIBRARY_PATH\" \
@@ -1068,9 +1068,9 @@
                            " -max-threads " ^ string_of_int max_threads
                          else
                            "") ^
-                        " < " ^ Path.implode in_path ^
-                        " > " ^ Path.implode out_path ^
-                        " 2> " ^ Path.implode err_path)
+                        " < " ^ File.shell_path in_path ^
+                        " > " ^ File.shell_path out_path ^
+                        " 2> " ^ File.shell_path err_path)
               val (ps, nontriv_js) = read_output_file out_path
                                      |>> map (apfst reindex) ||> map reindex
               val js = triv_js @ nontriv_js