equal
deleted
inserted
replaced
136 my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000); |
136 my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000); |
137 |
137 |
138 my $thy_text = join("", @lines); |
138 my $thy_text = join("", @lines); |
139 my $old_len = length($thy_text); |
139 my $old_len = length($thy_text); |
140 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; |
140 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; |
|
141 $thy_text =~ s/\b$thy_name\./$new_thy_name./g; |
141 $thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g; |
142 $thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g; |
142 die "No 'imports' found" if length($thy_text) == $old_len; |
143 die "No 'imports' found" if length($thy_text) == $old_len; |
143 |
144 |
144 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; |
145 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; |
145 print NEW_FILE $thy_text; |
146 print NEW_FILE $thy_text; |