equal
deleted
inserted
replaced
106 |
106 |
107 open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; |
107 open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; |
108 my @lines = <OLD_FILE>; |
108 my @lines = <OLD_FILE>; |
109 close(OLD_FILE); |
109 close(OLD_FILE); |
110 |
110 |
|
111 my $setup_import = |
|
112 substr("\"$output_path\/$setup_thy_name\"" . (" " x 1000), 0, 1000); |
|
113 |
111 my $thy_text = join("", @lines); |
114 my $thy_text = join("", @lines); |
112 my $old_len = length($thy_text); |
115 my $old_len = length($thy_text); |
113 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; |
116 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; |
114 $thy_text =~ s/(imports)(\s+)/$1 "$output_path\/$setup_thy_name"$2/g; |
117 $thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g; |
115 die "No 'imports' found" if length($thy_text) == $old_len; |
118 die "No 'imports' found" if length($thy_text) == $old_len; |
116 |
119 |
117 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; |
120 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; |
118 print NEW_FILE $thy_text; |
121 print NEW_FILE $thy_text; |
119 close(NEW_FILE); |
122 close(NEW_FILE); |