X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtLexer.mll;fp=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtLexer.mll;h=0000000000000000000000000000000000000000;hb=f12f1b61a608140a65990d36045d978575b2dcb0;hp=dc293bdcffef1953c1bec72d0c342df04a18be15;hpb=2b1375e4b44e2ef351a6341a5bb0a4823e8daae5;p=helm.git

diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll
deleted file mode 100644
index dc293bdcf..000000000
--- a/helm/software/lambda-delta/text/txtLexer.mll
+++ /dev/null
@@ -1,72 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-{ 
-   module L = Log
-   module O = Options
-   module P = TxtParser
-   
-   let out s = if !O.debug_lexer then L.warn s else ()
-}
-
-let BS    = "\\"
-let SPC   = [' ' '\t' '\n']+
-let OC    = "\\*"
-let CC    = "*\\"
-let FIG   = ['0'-'9']
-let ALPHA = ['A'-'Z' 'a'-'z' '_']
-let QT    = '"'
-let ID    = ALPHA+ (ALPHA | FIG)*
-let IX    = FIG+
-
-rule block_comment = parse
-   | CC  { () }
-   | OC  { block_comment lexbuf; block_comment lexbuf }
-   | _   { block_comment lexbuf }
-and qstring = parse
-   | QT    { ""                                }
-   | SPC   { " " ^ qstring lexbuf              }  
-   | BS BS { "\\" ^ qstring lexbuf             } 
-   | 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     }