src/HOL/Mirabelle/lib/scripts/mirabelle.pl
changeset 62779 7737e26cd3c6
parent 62677 0df43889f496
child 66156 f54c32c413a9
equal deleted inserted replaced
62778:f0e8ed202ce5 62779:7737e26cd3c6
   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;