X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtLexer.mll;fp=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtLexer.mll;h=05637286e81e73490e2845bcb4f9a5cf6719d05d;hb=689118326fbe47231865b26c66ae89144459be6a;hp=6a53d828f5b08172ceb7fbef405c31ff30cba7cc;hpb=797a122af3ff4a9682bf77a0fb05ecfb0f9effde;p=helm.git

diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll
index 6a53d828f..05637286e 100644
--- a/helm/software/lambda-delta/text/txtLexer.mll
+++ b/helm/software/lambda-delta/text/txtLexer.mll
@@ -38,25 +38,30 @@ 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         { out "ID"; P.ID (Lexing.lexeme lexbuf)                 }
-   | IX         { out "IX"; P.IX (int_of_string (Lexing.lexeme lexbuf)) }
-   | QT         { let s = qstring lexbuf in out "STR"; P.STR s          }
-   | "\\open"   { out "OPEN"; P.OPEN     } 
-   | "\\close"  { out "CLOSE"; P.CLOSE   }
-   | "\\global" { out "GLOBAL"; P.GLOBAL }
-   | "("        { 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     }
-   | 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       }
+   | "\\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   }
+   | eof       { out "EOF"; P.EOF     }