doc-src/TutorialI/Overview/LNCS/makeDemo

Sort search results in order of relevance, where relevance =
a) better if 0 premises for intro or 1 premise for elim/dest rules
b) better if substitution size wrt to current goal is smaller

Only applies to intro, dest, elim, and simp

(contributed by Rafal Kolanski, NICTA)

#!/usr/bin/perl -w

sub doit {
    my ($file) = @_;

    open (FILE, $file) || die $!;
    undef $/; $text = <FILE>; $/ = "\n";
    close FILE || die $!;

    $_ = $text;

    s/text_raw\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
    s/text\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
    s/\(\*<\*\)//sg;
    s/\(\*>\*\)//sg;

    $result = $_;

    if ($text ne $result) {
        print STDERR "fixing $file\n";
#        if (! -f "$file~~") {
#            rename $file, "$file~~" || die $!;
#        }
        open (FILE, "> Demo/$file") || die $!;
        print FILE $result;
        close FILE || die $!;
    }
}


foreach $file (@ARGV) {
  eval { &doit($file); };
  if ($@) { print STDERR "*** doit $file: ", $@, "\n"; }
}