# HG changeset patch
# User krauss
# Date 1300707803 -3600
# Node ID 60350051ef935aaf782940b90839a9b4a244de0a
# Parent  143f3719491102573f678ae3e5a2b05d58883694
mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)

diff -r 143f37194911 -r 60350051ef93 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 08:29:16 2011 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 12:43:23 2011 +0100
@@ -31,8 +31,9 @@
   $end_line = $3;
 }
 my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
-my $new_thy_name = $thy_name . "_Mirabelle";
-my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
+my $rand_suffix = map { ('a'..'z')[rand(26)] } 1 .. 10;
+my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
+my $new_thy_file = $path . "/" . $new_thy_name . $ext;
 
 
 # setup
@@ -108,7 +109,7 @@
 my $thy_text = join("", @lines);
 my $old_len = length($thy_text);
 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
-$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
+$thy_text =~ s/(imports)(\s+)/$1 "$output_path\/$setup_thy_name"$2/g;
 die "No 'imports' found" if length($thy_text) == $old_len;
 
 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
@@ -117,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 \"$output_path/$new_thy_name\";\n";
+print ROOT_FILE "use_thy \"$path/$new_thy_name\";\n";
 close(ROOT_FILE);
 
 
@@ -147,5 +148,6 @@
 
 unlink $root_file;
 unlink $setup_file;
+unlink $new_thy_file;
 
 exit $result;