# HG changeset patch
# User schirmer
# Date 1075127631 -3600
# Node ID b378b6faf4a7613da183afcf737864f2e7ffa025
# Parent  ad2f5da643b47bb788f608e68955b341cd971a95
\\<...> will be converted to \<...>
\\<^...> will be converted to \<^...>

diff -r ad2f5da643b4 -r b378b6faf4a7 lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Mon Jan 26 10:34:02 2004 +0100
+++ b/lib/scripts/convert.pl	Mon Jan 26 15:33:51 2004 +0100
@@ -8,7 +8,6 @@
 #   produces from each input file (on the command line) a new file with
 #   ".thy" appended and renames the original input file by appending "~0~"
 
-
 sub thmlist {
   my $s = shift;
   $s =~ s/^\[(.*)\]$/$1/sg;
@@ -236,7 +235,6 @@
     open(ARGVOUT, '>'.$tmpfile);
     select(ARGVOUT);
   }
-
  nl:
   if(!s/;(\s*?(\n?$|\(\*))/$1/s && !eof()) {# no end_of_ML_command marker
     $_ = $_ . <>;
@@ -247,9 +245,11 @@
   m/^(\s*)(.*?)(\s*)$/s;
   $head=$1; $line=$2; $tail=$3;
   $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
+  $line =~ s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...>
   print $head; $_=$line.$tail;
   if ($line =~ m/^\(\*/) { # start comment
     while (($i = index $_,"*)") == -1 && !eof()) { # no end comment
+      s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...>
       print;
       $_ = <>;
     }