# HG changeset patch
# User haftmann
# Date 1118666105 -7200
# Node ID 4fc8d8c99e9ef18d7e3e10e63ca5bae75b748c47
# Parent  f53ccd0cc70edf67cc16f4278216c225ef9e9e8b
experimental

diff -r f53ccd0cc70e -r 4fc8d8c99e9e Admin/isa-migrate
--- a/Admin/isa-migrate	Mon Jun 13 14:31:21 2005 +0200
+++ b/Admin/isa-migrate	Mon Jun 13 14:35:05 2005 +0200
@@ -24,15 +24,48 @@
     thyheader => sub {
         my ($file, @content) = @_;
         $_ = join("", @content);
-        if (m!\G
-                ^
-                    theory\s+([^ ]+)
-                    (?:\s+(?:imports|=)\s+([^:]*?))?
-                    (?:\s+(?:files|uses)\s+([^:]*?))?
-                    \s*(?:begin|:)
-             !cgomsx) {
-            # STRATEGIE: abschnittsweises matchen, zwischendurch immer wieder whitespace
-            # verarbeiten
+        if (m!^theory!cgoms) {
+            my $prelude = $';
+            my $thyheader = "theory";
+            $thyheader .= skip_wscomment();
+            if (m!\G(\S+)!cgoms) {
+                $thyheader .= $1;
+                $thyheader .= skip_wscomment();
+                print "--->\n>>>$thyheader<<<\n<---\n";
+                if (m!\G(?:imports|=)!cgoms) {
+                    $thyheader .= "imports";
+                    $thyheader .= skip_wscomment() || " ";
+                    print "--->\n>>>$thyheader<<<\n<---\n";
+                    while () {
+                        my $str = read_plainstring();
+                        print "--->\n>>>$str<<<\n<---\n";
+                        if (! $str) {
+                            last;
+                        }
+                        $thyheader .= $str;
+                        $thyheader .= skip_wscomment();
+                    }
+                    #~ print "--->\n>>>$thyheader<<<\n<---\n";
+                }
+                if (m!\G(?:files|uses)!cgoms) {
+                    $thyheader .= "uses";
+                    $thyheader .= skip_wscomment();
+                    while () {
+                        my $str = read_plainstring();
+                        if (! $str) {
+                            last;
+                        }
+                        $thyheader .= $str;
+                        $thyheader .= skip_wscomment();
+                    }
+                }
+                if (m!\G(?:begin|:)!cgoms) {
+                    my $postlude = $';
+                    $thyheader .=  "begin";
+                    # do replacement here
+                    print "$file:\n$thyheader\n\n";
+                }
+            }
         }
     }
 );
@@ -64,6 +97,11 @@
     }
 }
 
+sub read_plainstring {
+    m!\G("[^"]+"|[^"\s]+)!cgoms or return "";
+    return $&;
+}
+
 # process dir tree
 sub process_tree {
     my ($root, $migrator, $backupext) = @_;