mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
authorkrauss
Mon Mar 21 12:43:23 2011 +0100 (2011-03-21)
changeset 4203360350051ef93
parent 42032 143f37194911
child 42034 a77df5241959
mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
     1.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 08:29:16 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 12:43:23 2011 +0100
     1.3 @@ -31,8 +31,9 @@
     1.4    $end_line = $3;
     1.5  }
     1.6  my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
     1.7 -my $new_thy_name = $thy_name . "_Mirabelle";
     1.8 -my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;
     1.9 +my $rand_suffix = map { ('a'..'z')[rand(26)] } 1 .. 10;
    1.10 +my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
    1.11 +my $new_thy_file = $path . "/" . $new_thy_name . $ext;
    1.12  
    1.13  
    1.14  # setup
    1.15 @@ -108,7 +109,7 @@
    1.16  my $thy_text = join("", @lines);
    1.17  my $old_len = length($thy_text);
    1.18  $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
    1.19 -$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
    1.20 +$thy_text =~ s/(imports)(\s+)/$1 "$output_path\/$setup_thy_name"$2/g;
    1.21  die "No 'imports' found" if length($thy_text) == $old_len;
    1.22  
    1.23  open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
    1.24 @@ -117,7 +118,7 @@
    1.25  
    1.26  my $root_file = "$output_path/ROOT_$thy_name.ML";
    1.27  open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
    1.28 -print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n";
    1.29 +print ROOT_FILE "use_thy \"$path/$new_thy_name\";\n";
    1.30  close(ROOT_FILE);
    1.31  
    1.32  
    1.33 @@ -147,5 +148,6 @@
    1.34  
    1.35  unlink $root_file;
    1.36  unlink $setup_file;
    1.37 +unlink $new_thy_file;
    1.38  
    1.39  exit $result;