- conditional compilation continues ...

[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 67d8ccd55b974433fbb03a43d67d8a1c8dd6ce40..5a7155e4a56db66a0aa153c02b9b8cd121180856 100644 (file)
--- a/helm/software/helena/src/automath/autLexer.mll
+++ b/helm/software/helena/src/automath/autLexer.mll
@@ -15,9 +15,12 @@
    module AP = AutParser
 
    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
@@ -29,6 +32,8 @@
            id
       in
       aux 0
+
+END
 }
 
 let LC  = ['#' '%']
@@ -52,41 +57,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     }