refactoring ...

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

diff --git a/helm/software/lambda-delta/src/automath/autLexer.mll b/helm/software/lambda-delta/src/automath/autLexer.mll
deleted file mode 100644 (file)
index c0bc55a..0000000
--- a/helm/software/lambda-delta/src/automath/autLexer.mll
+++ /dev/null
@@ -1,90 +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 G  = Options
-   module AP = AutParser
-   
-   let out s = if !G.debug_lexer then L.warn s else ()
-
-(* This turns an Automath identifier into an XML nmtoken *)
-   let quote id =
-      let l = String.length id in
-      let rec aux i =
-         if i < l then begin
-            if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
-           aux (succ i)
-         end else
-           id
-      in
-      aux 0
-}
-
-let LC  = ['#' '%']
-let OC  = "{"
-let CC  = "}"
-let SPC = [' ' '\t' '\n']+
-let NL  = "\n"
-let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
-
-rule line_comment = parse
-   | NL  { () }
-   | OC  { block_comment lexbuf; line_comment lexbuf }
-   | _   { line_comment lexbuf }
-   | eof { () } 
-and block_comment = parse
-   | CC  { () }
-   | OC  { block_comment lexbuf; block_comment lexbuf }
-   | LC  { line_comment lexbuf; block_comment lexbuf  }
-   | _   { block_comment lexbuf }
-and token = parse
-   | SPC      { token lexbuf } 
-   | LC       { line_comment lexbuf; token lexbuf  }
-   | OC       { block_comment lexbuf; token lexbuf }
-   | "_E"     { out "E"; AP.E         }
-   | "'_E'"   { out "E"; AP.E         }
-   | "---"    { out "EB"; AP.EB       }
-   | "'eb'"   { out "EB"; AP.EB       }
-   | "EB"     { out "EB"; AP.EB       }
-   | "--"     { out "EXIT"; AP.EXIT   }
-   | "PN"     { out "PN"; AP.PN       }
-   | "'pn'"   { out "PN"; AP.PN       }
-   | "PRIM"   { out "PN"; AP.PN       }
-   | "'prim'" { out "PN"; AP.PN       }
-   | "???"    { out "PN"; AP.PN       }
-   | "PROP"   { out "PROP"; AP.PROP   }
-   | "'prop'" { out "PROP"; AP.PROP   }
-   | "TYPE"   { out "TYPE"; AP.TYPE   }
-   | "'type'" { out "TYPE"; AP.TYPE   }
-   | ID       { out "ID"; 
-                   let s = Lexing.lexeme lexbuf in
-                   if !G.unquote then AP.IDENT s else AP.IDENT (quote s)
-              }
-   | ":="     { out "DEF"; AP.DEF     }
-   | "("      { out "OP"; AP.OP       }
-   | ")"      { out "CP"; AP.CP       }
-   | "["      { out "OB"; AP.OB       }
-   | "]"      { out "CB"; AP.CB       }
-   | "<"      { out "OA"; AP.OA       }
-   | ">"      { out "CA"; AP.CA       }
-   | "@"      { out "AT"; AP.AT       }
-   | "~"      { out "TD"; AP.TD       }
-   | "\""     { out "QT"; AP.QT       }
-   | ":"      { out "CN"; AP.CN       }   
-   | ","      { out "CM"; AP.CM       }
-   | ";"      { out "SC"; AP.SC       }
-   | "."      { out "FS"; AP.FS       }   
-   | "+"      { out "PLUS"; AP.PLUS   }
-   | "-"      { out "MINUS"; AP.MINUS }
-   | "*"      { out "TIMES"; AP.TIMES }
-   | "="      { out "DEF"; AP.DEF     }
-   | eof      { out "EOF"; AP.EOF     }