X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautLexer.mll;h=58324a0216c71e2c693a3d0ca5169a2a7a193e93;hb=2976c347e18717e691825ebdf73a5ce941c57d1b;hp=c0bc55afd2bd292ad96031fa3d8259d5ccdfb5b9;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll
index c0bc55afd..58324a021 100644
--- a/helm/software/helena/src/automath/autLexer.mll
+++ b/helm/software/helena/src/automath/autLexer.mll
@@ -10,23 +10,29 @@
       V_______________________________________________________________ *)
 
 { 
+   module KT = String
+
    module L  = Log
    module G  = Options
    module AP = AutParser
-   
-   let out s = if !G.debug_lexer then L.warn s else ()
 
+   let level = 0
+
+IFDEF LEXER THEN   
+   let out s = if !G.debug_lexer then L.warn level s else ()
+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
 }
 
 let LC  = ['#' '%']
@@ -50,41 +56,45 @@ and token = parse
    | SPC      { token lexbuf } 
    | LC       { line_comment lexbuf; token lexbuf  }
    | OC       { block_comment lexbuf; token lexbuf }
-   | "_E"     { out "E"; AP.E         }
-   | "'_E'"   { out "E"; AP.E         }
-   | "---"    { out "EB"; AP.EB       }
-   | "'eb'"   { out "EB"; AP.EB       }
-   | "EB"     { out "EB"; AP.EB       }
-   | "--"     { out "EXIT"; AP.EXIT   }
-   | "PN"     { out "PN"; AP.PN       }
-   | "'pn'"   { out "PN"; AP.PN       }
-   | "PRIM"   { out "PN"; AP.PN       }
-   | "'prim'" { out "PN"; AP.PN       }
-   | "???"    { out "PN"; AP.PN       }
-   | "PROP"   { out "PROP"; AP.PROP   }
-   | "'prop'" { out "PROP"; AP.PROP   }
-   | "TYPE"   { out "TYPE"; AP.TYPE   }
-   | "'type'" { out "TYPE"; AP.TYPE   }
-   | ID       { out "ID"; 
+   | "_E"     { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
+   | "'_E'"   { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
+   | "---"    { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
+   | "'eb'"   { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
+   | "EB"     { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
+   | "--"     { IFDEF LEXER THEN out "EXIT" ELSE () END; AP.EXIT   }
+   | "PN"     { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
+   | "'pn'"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
+   | "PRIM"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
+   | "'prim'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
+   | "???"    { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
+   | "PROP"   { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
+   | "'prop'" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
+   | "TYPE"   { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
+   | "'type'" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
+   | ID       { IFDEF LEXER THEN out "ID" ELSE () END; 
                    let s = Lexing.lexeme lexbuf in
-                   if !G.unquote then AP.IDENT s else AP.IDENT (quote s)
+IFDEF QUOTE THEN
+                   if !G.quote then AP.IDENT (quote s) else AP.IDENT s
+ELSE
+                   AP.IDENT s
+END
               }
-   | ":="     { out "DEF"; AP.DEF     }
-   | "("      { out "OP"; AP.OP       }
-   | ")"      { out "CP"; AP.CP       }
-   | "["      { out "OB"; AP.OB       }
-   | "]"      { out "CB"; AP.CB       }
-   | "<"      { out "OA"; AP.OA       }
-   | ">"      { out "CA"; AP.CA       }
-   | "@"      { out "AT"; AP.AT       }
-   | "~"      { out "TD"; AP.TD       }
-   | "\""     { out "QT"; AP.QT       }
-   | ":"      { out "CN"; AP.CN       }   
-   | ","      { out "CM"; AP.CM       }
-   | ";"      { out "SC"; AP.SC       }
-   | "."      { out "FS"; AP.FS       }   
-   | "+"      { out "PLUS"; AP.PLUS   }
-   | "-"      { out "MINUS"; AP.MINUS }
-   | "*"      { out "TIMES"; AP.TIMES }
-   | "="      { out "DEF"; AP.DEF     }
-   | eof      { out "EOF"; AP.EOF     }
+   | ":="     { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
+   | "("      { IFDEF LEXER THEN out "OP" ELSE () END; AP.OP       }
+   | ")"      { IFDEF LEXER THEN out "CP" ELSE () END; AP.CP       }
+   | "["      { IFDEF LEXER THEN out "OB" ELSE () END; AP.OB       }
+   | "]"      { IFDEF LEXER THEN out "CB" ELSE () END; AP.CB       }
+   | "<"      { IFDEF LEXER THEN out "OA" ELSE () END; AP.OA       }
+   | ">"      { IFDEF LEXER THEN out "CA" ELSE () END; AP.CA       }
+   | "@"      { IFDEF LEXER THEN out "AT" ELSE () END; AP.AT       }
+   | "~"      { IFDEF LEXER THEN out "TD" ELSE () END; AP.TD       }
+   | "\""     { IFDEF LEXER THEN out "QT" ELSE () END; AP.QT       }
+   | ":"      { IFDEF LEXER THEN out "CN" ELSE () END; AP.CN       }   
+   | ","      { IFDEF LEXER THEN out "CM" ELSE () END; AP.CM       }
+   | ";"      { IFDEF LEXER THEN out "SC" ELSE () END; AP.SC       }
+   | "."      { IFDEF LEXER THEN out "FS" ELSE () END; AP.FS       }   
+   | "+"      { IFDEF LEXER THEN out "PLUS" ELSE () END; AP.PLUS   }
+   | "-"      { IFDEF LEXER THEN out "MINUS" ELSE () END; AP.MINUS }
+   | "*"      { IFDEF LEXER THEN out "TIMES" ELSE () END; AP.TIMES }
+   | "="      { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
+   | eof      { IFDEF LEXER THEN out "EOF" ELSE () END; AP.EOF     }