- final commit for helena 0.8.3

[helm.git] / helm / software / helena / src / automath / autLexer.mll

diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll
index 5a7155e4a56db66a0aa153c02b9b8cd121180856..58324a0216c71e2c693a3d0ca5169a2a7a193e93 100644 (file)
--- a/helm/software/helena/src/automath/autLexer.mll
+++ b/helm/software/helena/src/automath/autLexer.mll
@@ -10,6 +10,8 @@
       V_______________________________________________________________ *)
 
 { 
+   module KT = String
+
    module L  = Log
    module G  = Options
    module AP = AutParser
@@ -23,15 +25,12 @@ END
 IFDEF QUOTE THEN
 (* This turns an Automath identifier into an XML nmtoken *)
    let quote id =
-      let l = String.length id in
-      let rec aux i =
-         if i < l then begin
-            if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
-           aux (succ i)
-         end else
-           id
+      let map = function
+         | '\''
+         | '`' -> '_';
+         | c   -> c
       in
-      aux 0
+      KT.map map id
 
 END
 }