equal
deleted
inserted
replaced
156 } |
156 } |
157 |
157 |
158 if ($output_log) { print "Mirabelle: $thy_file\n"; } |
158 if ($output_log) { print "Mirabelle: $thy_file\n"; } |
159 |
159 |
160 my $cmd = |
160 my $cmd = |
161 "\"$ENV{'ISABELLE_TOOL'}\" process " . |
161 "isabelle process -o quick_and_dirty -o threads=1" . |
162 "-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet; |
162 " -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet; |
163 my $result = system "bash", "-c", $cmd; |
163 my $result = system "bash", "-c", $cmd; |
164 |
164 |
165 if ($output_log) { |
165 if ($output_log) { |
166 my $outcome = ($result ? "failure" : "success"); |
166 my $outcome = ($result ? "failure" : "success"); |
167 print "\nFinished: $thy_file [$outcome]\n"; |
167 print "\nFinished: $thy_file [$outcome]\n"; |