reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path

--- a/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML	Tue Apr 24 12:36:27 2012 +0200
+++ b/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML	Tue Apr 24 13:56:13 2012 +0200
@@ -285,7 +285,7 @@
   )
 
 fun str_of_pos (pos, triv) =
-  str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
+  str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^
   (if triv then "[T]" else "")
 
 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,

--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Apr 24 12:36:27 2012 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Apr 24 13:56:13 2012 +0200
@@ -108,10 +108,13 @@
 my @lines = <OLD_FILE>;
 close(OLD_FILE);
 
+my $setup_import =
+  substr("\"$output_path\/$setup_thy_name\"" . (" " x 1000), 0, 1000);
+
 my $thy_text = join("", @lines);
 my $old_len = length($thy_text);
 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
-$thy_text =~ s/(imports)(\s+)/$1 "$output_path\/$setup_thy_name"$2/g;
+$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
 die "No 'imports' found" if length($thy_text) == $old_len;
 
 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";