eliminated unnecessary generated ROOT.ML
authorkrauss
Mon Mar 21 14:37:10 2011 +0100 (2011-03-21)
changeset 420371571fde21911
parent 42036 a14e9cf805e0
child 42038 626fcf4a803e
eliminated unnecessary generated ROOT.ML
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
     1.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 14:25:59 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 14:37:10 2011 +0100
     1.3 @@ -116,11 +116,6 @@
     1.4  print NEW_FILE $thy_text;
     1.5  close(NEW_FILE);
     1.6  
     1.7 -my $root_file = "$output_path/ROOT_$thy_name.ML";
     1.8 -open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
     1.9 -print ROOT_FILE "use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n";
    1.10 -close(ROOT_FILE);
    1.11 -
    1.12  
    1.13  # run isabelle
    1.14  
    1.15 @@ -139,14 +134,13 @@
    1.16  print "Mirabelle: $thy_file\n" if ($quiet ne "");
    1.17  
    1.18  my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
    1.19 -  "-e 'use \"$root_file\";' -q $mirabelle_logic" . $quiet;
    1.20 +  "-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
    1.21  
    1.22  print "Finished:  $thy_file\n" if ($quiet ne "");
    1.23  
    1.24  
    1.25  # cleanup
    1.26  
    1.27 -unlink $root_file;
    1.28  unlink $setup_file;
    1.29  unlink $new_thy_file;
    1.30