lib/scripts/fixheaders.pl
changeset 18125 50e63c68768f
parent 16703 40a0b3187807
equal deleted inserted replaced
18124:a310c78298f9 18125:50e63c68768f
    22     open(ISTREAM, $file) or die $!;
    22     open(ISTREAM, $file) or die $!;
    23     my @content = <ISTREAM>;
    23     my @content = <ISTREAM>;
    24     close ISTREAM or die $!;
    24     close ISTREAM or die $!;
    25     my $content = join("", @content);
    25     my $content = join("", @content);
    26     $_ = $content;
    26     $_ = $content;
    27     if (m!^theory!cgoms) {
    27     if (m!^(\s*theory)!cgoms) {
    28         my $prelude = $`;
    28         my $prelude = $`;
    29         my $thyheader = "theory";
    29         my $thyheader = $1;
    30         $thyheader .= skip_wscomment();
    30         $thyheader .= skip_wscomment();
    31         if (m!\G(\S+)!cgoms) {
    31         if (m!\G(\S+)!cgoms) {
    32             $thyheader .= $1;
    32             $thyheader .= $1;
    33             $thyheader .= skip_wscomment();
    33             $thyheader .= skip_wscomment();
    34             if (m!\G(?:imports|=)!cgoms) {
    34             if (m!\G(?:imports|=)!cgoms) {