From c340ab85b58833bfe5cba251b6df93e674d1cde6 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 12 Dec 2007 18:13:14 +0000 Subject: [PATCH] add support for adding identifiers instead of only changing them (enabled per default) --- helm/software/matita/rottener.ml | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) 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) -- 2.39.2