From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Nov 2007 09:27:01 +0000 (+0000)
Subject: - use "O" as the rottening token
X-Git-Tag: make_still_working~5770
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca351b377ef8cb69ef712df0050620f75d4b649a;p=helm.git

- use "O" as the rottening token
- add generation of a trailer with error location information
---

diff --git a/helm/software/matita/rottener.ml b/helm/software/matita/rottener.ml
index 7114f018d..9888e11e7 100644
--- a/helm/software/matita/rottener.ml
+++ b/helm/software/matita/rottener.ml
@@ -28,6 +28,9 @@ open Printf
 module Ast = GrafiteAst
 module Pt = CicNotationPt
 
+let error_token = "O"
+let error_token_len = String.length error_token
+
 let has_toplevel_term = function
   | GrafiteParser.LSome (Ast.Executable (_, Ast.Command (_, Ast.Obj (loc, (
         Pt.Theorem ((`Definition | `Lemma | `Theorem), _, _, _)
@@ -74,18 +77,28 @@ let rotten_script ~fname statement =
         (sanitize_tokens tokens) in
     List.nth idents (Random.int (List.length idents))
   in
+  let start_pos, end_pos =
+    Glib.Utf8.offset_to_pos statement 0 (Ploc.first_pos target_pos),
+    Glib.Utf8.offset_to_pos statement 0 (Ploc.last_pos target_pos) in
   let statement' =
     (* positions in bytecount *)
-    let start_pos, end_pos =
-      Glib.Utf8.offset_to_pos statement 0 (Ploc.first_pos target_pos),
-      Glib.Utf8.offset_to_pos statement 0 (Ploc.last_pos target_pos) in
     String.sub statement 0 start_pos
-    ^ "true"
-    ^ String.sub statement end_pos (String.length statement - end_pos)
-  in
+    ^ "O"
+    ^ String.sub statement end_pos (String.length statement - end_pos) in
   let script = HExtlib.input_file fname in
-  let script' =
-    Pcre.replace ~pat:(Pcre.quote statement) ~templ:statement' script in
+  let matches =
+    let rex =
+      Pcre.regexp ~flags:[`DOTALL]
+        (sprintf "^(.*)(%s)(.*)$" (Pcre.quote statement)) in
+    try
+      Pcre.extract ~rex script
+    with Not_found -> assert false
+  in
+  let trailer = (* trailing comment with machine parseable error location *)
+    let preamble_len = String.length matches.(1) in
+    sprintf "\n(*\nerror-at: %d-%d\n*)\n" (preamble_len + start_pos)
+      (preamble_len + start_pos + error_token_len) in
+  let script' = sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
   let md5 = Digest.to_hex (Digest.string script') in
   HExtlib.output_file
     ~filename:(sprintf "%s.rottened.%s.ma" (Filename.chop_extension fname) md5)