doc-src/TutorialI/IsarOverview/Isar/makeDemo
author nipkow
Mon, 08 Jul 2002 08:20:21 +0200
changeset 13307 cf076cdcfbf3
child 13613 531f1f524848
permissions -rwxr-xr-x
*** empty log message ***

#!/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"; }
}