From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 12 Dec 2007 18:13:14 +0000 (+0000)
Subject: add support for adding identifiers instead of only changing them (enabled per default)
X-Git-Tag: make_still_working~5710
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c340ab85b58833bfe5cba251b6df93e674d1cde6;p=helm.git

add support for adding identifiers instead of only changing them (enabled per default)
---

diff --git a/helm/software/matita/rottener.ml b/helm/software/matita/rottener.ml
index 27c277664..dfb64037e 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
 
+  (* set to false to change identifier instead of adding extra identifiers *)
+let add_ident = ref true
+
 let error_token = "O"
 let error_token_len = String.length error_token
 
@@ -87,14 +90,19 @@ let rotten_script ~fname statement =
         (sanitize_tokens [] tokens) in
     List.nth idents (Random.int (List.length idents))
   in
-  let start_pos, end_pos =
+  let start_pos, end_pos =  (* positions in bytecount *)
     Glib.Utf8.offset_to_pos statement 0 (Stdpp.first_pos target_pos),
     Glib.Utf8.offset_to_pos statement 0 (Stdpp.last_pos target_pos) in
   let statement' =
-    (* positions in bytecount *)
-    String.sub statement 0 start_pos
-    ^ "O"
-    ^ String.sub statement end_pos (String.length statement - end_pos) in
+    if !add_ident then
+      String.sub statement 0 start_pos
+      ^ "O "
+      ^ String.sub statement start_pos (String.length statement - start_pos)
+    else
+      String.sub statement 0 start_pos
+      ^ "O"
+      ^ String.sub statement end_pos (String.length statement - end_pos)
+  in
   let script = HExtlib.input_file fname in
   let matches =
     let rex =
@@ -107,9 +115,10 @@ let rotten_script ~fname statement =
   let trailer = (* trailing comment with machine parseable error location *)
     let preamble_len = Glib.Utf8.length matches.(1) in
     sprintf "\n(*\nerror-at: %d-%d\n*)\n"
-    (preamble_len + Stdpp.first_pos target_pos)
-    (preamble_len + Stdpp.first_pos target_pos + error_token_len) in
-  let script' = sprintf "%s%s%s%s" matches.(1) statement' matches.(3) trailer in
+      (preamble_len + Stdpp.first_pos target_pos)
+      (preamble_len + Stdpp.first_pos target_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.%s.rottened" fname md5)