- we completed the text parser fixing the syntactic shortcuts

[helm.git] / helm / software / lambda-delta / automath / autLexer.mll

diff --git a/helm/software/lambda-delta/automath/autLexer.mll b/helm/software/lambda-delta/automath/autLexer.mll
index b7009f9240011a28392d02c760c7a7b8dade963d..51f1e7cb92513197a3619e524eab01fe4698884b 100644 (file)
--- a/helm/software/lambda-delta/automath/autLexer.mll
+++ b/helm/software/lambda-delta/automath/autLexer.mll
@@ -11,13 +11,12 @@
 
 { 
    module L = Log
+   module O = Options
    module P = AutParser
    
    let debug = false
    let out s = if debug then L.warn s else ()
 
-   let unquote = ref false
-
 (* This turns an Automath identifier into an XML nmtoken *)
    let quote id =
       let l = String.length id in
@@ -69,7 +68,7 @@ and token = parse
    | "'type'" { out "TYPE"; P.TYPE   }
    | ID       { out "ID"; 
                    let s = Lexing.lexeme lexbuf in
-                   if !unquote then P.IDENT s else P.IDENT (quote s)
+                   if !O.unquote then P.IDENT s else P.IDENT (quote s)
               }
    | ":="     { out "DEF"; P.DEF     }
    | "("      { out "OP"; P.OP       }