# HG changeset patch
# User krauss
# Date 1300707805 -3600
# Node ID a77df5241959ca9dbc84a543a7588db9cf84e9ea
# Parent  60350051ef935aaf782940b90839a9b4a244de0a
propagate mirabelle failures properly;
flatten obscure return code semantics of Perl system command to 0/1

diff -r 60350051ef93 -r a77df5241959 src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Mon Mar 21 12:43:23 2011 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Mon Mar 21 12:43:25 2011 +0100
@@ -56,6 +56,12 @@
   exit 1
 }
 
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
 
 ## process command line
 
@@ -103,6 +109,6 @@
 
 for FILE in "$@"
 do
-  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE"
+  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
 done
 
diff -r 60350051ef93 -r a77df5241959 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 12:43:23 2011 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 12:43:25 2011 +0100
@@ -118,7 +118,7 @@
 
 my $root_file = "$output_path/ROOT_$thy_name.ML";
 open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
-print ROOT_FILE "use_thy \"$path/$new_thy_name\";\n";
+print ROOT_FILE "use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n";
 close(ROOT_FILE);
 
 
@@ -150,4 +150,4 @@
 unlink $setup_file;
 unlink $new_thy_file;
 
-exit $result;
+exit ($result ? 1 : 0);