equal
deleted
inserted
replaced
62 val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else () |
62 val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else () |
63 val svc_input_file = File.tmp_path (Path.basic "SVM_in"); |
63 val svc_input_file = File.tmp_path (Path.basic "SVM_in"); |
64 val svc_output_file = File.tmp_path (Path.basic "SVM_out"); |
64 val svc_output_file = File.tmp_path (Path.basic "SVM_out"); |
65 val _ = File.write svc_input_file svc_input; |
65 val _ = File.write svc_input_file svc_input; |
66 val _ = |
66 val _ = |
67 bash_output (check_valid ^ " -dump-result " ^ |
67 Isabelle_System.bash_output (check_valid ^ " -dump-result " ^ |
68 File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^ |
68 File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^ |
69 ">/dev/null 2>&1") |
69 ">/dev/null 2>&1") |
70 val svc_output = |
70 val svc_output = |
71 (case try File.read svc_output_file of |
71 (case try File.read svc_output_file of |
72 SOME out => out |
72 SOME out => out |