]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/text/txtLexer.mll
hints polished and fixed to allow recursive inference of ext_carr
[helm.git] / helm / software / lambda-delta / src / text / txtLexer.mll
index dc293bdcffef1953c1bec72d0c342df04a18be15..e5ced380684b07046560d3a49e341c67432a1937 100644 (file)
       V_______________________________________________________________ *)
 
 { 
-   module L = Log
-   module O = Options
-   module P = TxtParser
+   module L  = Log
+   module  = Options
+   module TP = TxtParser
    
-   let out s = if !O.debug_lexer then L.warn s else ()
+   let out s = if !G.debug_lexer then L.warn s else ()
 }
 
 let BS    = "\\"
@@ -38,35 +38,35 @@ and qstring = parse
    | BS QT { "\"" ^ qstring lexbuf             }  
    | _ as c { String.make 1 c ^ qstring lexbuf }
 and token = parse
-   | SPC          { token lexbuf                                        } 
-   | OC           { block_comment lexbuf; token lexbuf                  }
-   | ID as id     { out ("ID " ^ id); P.ID id                           }
-   | IX as ix     { out ("IX " ^ ix); P.IX (int_of_string ix)           }
-   | QT           { let s = qstring lexbuf in out ("STR " ^ s); P.STR s }
-   | "\\graph"    { out "GRAPH"; P.GRAPH }
-   | "\\decl"     { out "DECL"; P.DECL   }
-   | "\\ax"       { out "AX"; P.AX       }
-   | "\\def"      { out "DEF"; P.DEF     }
-   | "\\th"       { out "TH"; P.TH       }
-   | "\\generate" { out "GEN"; P.GEN     }
-   | "\\require"  { out "REQ"; P.REQ     }
-   | "\\open"     { out "OPEN"; P.OPEN   } 
-   | "\\close"    { out "CLOSE"; P.CLOSE }
-   | "\\sorts"    { out "SORTS"; P.SORTS }
-   | "("          { out "OP"; P.OP       }
-   | ")"          { out "CP"; P.CP       }
-   | "["          { out "OB"; P.OB       }
-   | "]"          { out "CB"; P.CB       }
-   | "<"          { out "OA"; P.OA       }
-   | ">"          { out "CA"; P.CA       }
-   | "."          { out "FS"; P.FS       }   
-   | ":"          { out "CN"; P.CN       }   
-   | ","          { out "CM"; P.CM       }
-   | "="          { out "EQ"; P.EQ       }
-   | "*"          { out "STAR"; P.STAR   }
-   | "#"          { out "HASH"; P.HASH   }
-   | "+"          { out "PLUS"; P.PLUS   }
-   | "~"          { out "TE"; P.TE       }
-   | "->"         { out "WTO"; P.WTO     }
-   | "=>"         { out "STO"; P.STO     }
-   | eof          { out "EOF"; P.EOF     }
+   | SPC          { token lexbuf                                         
+   | OC           { block_comment lexbuf; token lexbuf                   }
+   | ID as id     { out ("ID " ^ id); TP.ID id                           }
+   | IX as ix     { out ("IX " ^ ix); TP.IX (int_of_string ix)           }
+   | QT           { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s }
+   | "\\graph"    { out "GRAPH"; TP.GRAPH }
+   | "\\decl"     { out "DECL"; TP.DECL   }
+   | "\\ax"       { out "AX"; TP.AX       }
+   | "\\def"      { out "DEF"; TP.DEF     }
+   | "\\th"       { out "TH"; TP.TH       }
+   | "\\generate" { out "GEN"; TP.GEN     }
+   | "\\require"  { out "REQ"; TP.REQ     }
+   | "\\open"     { out "OPEN"; TP.OPEN   } 
+   | "\\close"    { out "CLOSE"; TP.CLOSE }
+   | "\\sorts"    { out "SORTS"; TP.SORTS }
+   | "("          { out "OP"; TP.OP       }
+   | ")"          { out "CP"; TP.CP       }
+   | "["          { out "OB"; TP.OB       }
+   | "]"          { out "CB"; TP.CB       }
+   | "<"          { out "OA"; TP.OA       }
+   | ">"          { out "CA"; TP.CA       }
+   | "."          { out "FS"; TP.FS       }   
+   | ":"          { out "CN"; TP.CN       }   
+   | ","          { out "CM"; TP.CM       }
+   | "="          { out "EQ"; TP.EQ       }
+   | "*"          { out "STAR"; TP.STAR   }
+   | "#"          { out "HASH"; TP.HASH   }
+   | "+"          { out "PLUS"; TP.PLUS   }
+   | "~"          { out "TE"; TP.TE       }
+   | "->"         { out "WTO"; TP.WTO     }
+   | "=>"         { out "STO"; TP.STO     }
+   | eof          { out "EOF"; TP.EOF     }