]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/text/txtLexer.mll
Regular expressions.
[helm.git] / helm / software / lambda-delta / text / txtLexer.mll
index fc00064e586cf5664dea7d4783433b7621f1d25a..073fabcba31ffd244414179de60224c9785e46e6 100644 (file)
@@ -38,33 +38,35 @@ and qstring = parse
    | BS QT { "\"" ^ qstring lexbuf                 } 
    | _     { Lexing.lexeme lexbuf ^ qstring lexbuf }
 and token = parse
-   | SPC       { token lexbuf                                 } 
-   | OC        { block_comment lexbuf; token lexbuf           }
-   | ID as id  { out "ID"; P.ID id                            }
-   | IX as ix  { out "IX"; P.IX (int_of_string ix)            }
-   | QT        { let s = qstring lexbuf in out "STR"; 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       }
-   | "\\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"; P.ID id                            }
+   | IX as ix     { out "IX"; P.IX (int_of_string ix)            }
+   | QT           { let s = qstring lexbuf in out "STR"; 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     }