doc-src/TutorialI/IsarOverview/Isar/makeDemo
author nipkow
Sun, 29 Dec 2002 23:12:39 +0100
changeset 13768 1764a81b7a0a
parent 13613 531f1f524848
permissions -rwxr-xr-x
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13307
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     1
#!/usr/bin/perl -w
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     2
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     3
sub doit {
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     4
    my ($file) = @_;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     5
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     6
    open (FILE, $file) || die $!;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     7
    undef $/; $text = <FILE>; $/ = "\n";
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     8
    close FILE || die $!;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
     9
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    10
    $_ = $text;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    11
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    12
    s/text_raw\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    13
    s/text\{\*([^*]|\*[^}])*\*\}//sg;       # actual work done here
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    14
    s/\(\*<\*\)//sg;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    15
    s/\(\*>\*\)//sg;
13613
531f1f524848 *** empty log message ***
nipkow
parents: 13307
diff changeset
    16
    s/--(\ )*"([^"])*"//sg;
531f1f524848 *** empty log message ***
nipkow
parents: 13307
diff changeset
    17
    s/--(\ )*\{\*([^*]|\*[^}])*\*\}//sg;
13307
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    18
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    19
    $result = $_;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    20
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    21
    if ($text ne $result) {
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    22
        print STDERR "fixing $file\n";
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    23
#        if (! -f "$file~~") {
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    24
#            rename $file, "$file~~" || die $!;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    25
#        }
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    26
        open (FILE, "> Demo/$file") || die $!;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    27
        print FILE $result;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    28
        close FILE || die $!;
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    29
    }
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    30
}
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    31
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    32
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    33
foreach $file (@ARGV) {
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    34
  eval { &doit($file); };
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    35
  if ($@) { print STDERR "*** doit $file: ", $@, "\n"; }
cf076cdcfbf3 *** empty log message ***
nipkow
parents:
diff changeset
    36
}