\\<...> will be converted to \<...>
authorschirmer
Mon Jan 26 15:33:51 2004 +0100 (2004-01-26)
changeset 14362b378b6faf4a7
parent 14361 ad2f5da643b4
child 14363 2c116016f95d
\\<...> will be converted to \<...>
\\<^...> will be converted to \<^...>
lib/scripts/convert.pl
     1.1 --- a/lib/scripts/convert.pl	Mon Jan 26 10:34:02 2004 +0100
     1.2 +++ b/lib/scripts/convert.pl	Mon Jan 26 15:33:51 2004 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  #   produces from each input file (on the command line) a new file with
     1.5  #   ".thy" appended and renames the original input file by appending "~0~"
     1.6  
     1.7 -
     1.8  sub thmlist {
     1.9    my $s = shift;
    1.10    $s =~ s/^\[(.*)\]$/$1/sg;
    1.11 @@ -236,7 +235,6 @@
    1.12      open(ARGVOUT, '>'.$tmpfile);
    1.13      select(ARGVOUT);
    1.14    }
    1.15 -
    1.16   nl:
    1.17    if(!s/;(\s*?(\n?$|\(\*))/$1/s && !eof()) {# no end_of_ML_command marker
    1.18      $_ = $_ . <>;
    1.19 @@ -247,9 +245,11 @@
    1.20    m/^(\s*)(.*?)(\s*)$/s;
    1.21    $head=$1; $line=$2; $tail=$3;
    1.22    $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
    1.23 +  $line =~ s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...>
    1.24    print $head; $_=$line.$tail;
    1.25    if ($line =~ m/^\(\*/) { # start comment
    1.26      while (($i = index $_,"*)") == -1 && !eof()) { # no end comment
    1.27 +      s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...>
    1.28        print;
    1.29        $_ = <>;
    1.30      }