diff -r 9b74d0339c44 -r 11542bebe4d4 lib/scripts/mirabelle
--- a/lib/scripts/mirabelle	Wed Aug 12 00:26:01 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-#!/usr/bin/perl -w
-
-use strict;
-use File::Basename;
-
-# Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html
-sub trim {
-    my @out = @_;
-    for (@out) {
-        s/^\s+//;
-        s/\s+$//;
-    }
-    return wantarray ? @out : $out[0];
-}
-
-sub quote {
-    my $str = pop;
-    return "\"" . $str . "\"";
-}
-
-sub print_usage_and_quit {
-    print STDERR "Usage: mirabelle actions file1.thy...\n" .
-                 "  actions: action1:...:actionN\n" .
-                 "  action: name or name[key1=value1,...,keyM=valueM]\n";
-    exit 1;
-}
-
-my $num_args = $#ARGV + 1;
-if ($num_args < 2) {
-    print_usage_and_quit();
-}
-
-my @action_names;
-my @action_settings;
-
-foreach (split(/:/, $ARGV[0])) {
-    my %settings;
-
-    $_ =~ /([^[]*)(?:\[(.*)\])?/;
-    my ($name, $settings_str) = ($1, $2 || "");
-    my @setting_strs = split(/,/, $settings_str);
-    foreach (@setting_strs) {
-        $_ =~ /(.*)=(.*)/;
-	    my $key = $1;
-	    my $value = $2;
-	    $settings{trim($key)} = trim($value);
-    }
-
-    push @action_names, trim($name);
-    push @action_settings, \%settings;
-}
-
-my $output_path = "/tmp/mirabelle"; # FIXME: generate path
-my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup";
-my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy";
-my $mirabelle_log_file = $output_path . "/mirabelle.log";
-
-mkdir $output_path, 0755;
-
-open(FILE, ">$mirabellesetup_file")
-    || die "Could not create file '$mirabellesetup_file'";
-
-my $invoke_lines;
-
-for my $i (0 .. $#action_names) { 
-    my $settings_str = "";
-    my $settings = $action_settings[$i];
-    my $key;
-    my $value;
-
-    while (($key, $value) = each(%$settings)) {
-        $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), ";
-    }
-    $settings_str =~ s/, $//;
-
-    $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" ";
-    $invoke_lines .= "[$settings_str] *}\n"
-}
-
-print FILE <<EOF;
-theory MirabelleSetup
-imports Mirabelle
-begin
-
-setup {* Mirabelle.set_logfile "$mirabelle_log_file" *}
-
-$invoke_lines
-
-end
-EOF
-
-my $root_text = "";
-my @new_thy_files;
-
-for my $i (1 .. $num_args - 1) {
-    my $old_thy_file = $ARGV[$i];
-    my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy");
-    my $new_thy_name = $base . "Mirabelle";
-    my $new_thy_file = $dir . $new_thy_name . $ext;
-
-    open(OLD_FILE, "<$old_thy_file")
-        || die "Cannot open file $old_thy_file";
-    my @lines = <OLD_FILE>;
-    close(OLD_FILE);
-
-    my $thy_text = join("", @lines);
-    my $old_len = length($thy_text);
-    $thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$mirabellesetup_thy_name" /gm;
-    die "No 'imports' found" if length($thy_text) == $old_len;
-
-    open(NEW_FILE, ">$new_thy_file");
-    print NEW_FILE $thy_text;
-    close(NEW_FILE);
-
-    $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n";
-
-    push @new_thy_files, $new_thy_file;
-}
-
-my $root_file = "ROOT_mirabelle.ML";
-open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file";
-print ROOT_FILE $root_text;
-close(ROOT_FILE);
-
-system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL";
-
-# unlink $mirabellesetup_file;
-unlink $root_file;
-unlink @new_thy_files;