helm/software/helena/src/text/txtLexer.mll

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 {
  13    module L  = Log
  14    module G  = Options
  15    module TP = TxtParser
  16
  17    let level = 0
  18
  19 IFDEF LEXER THEN
  20    let out s = if !G.debug_lexer then L.warn level s else ()
  21 END
  22 }
  23
  24 let BS    = "\\"
  25 let SPC   = [' ' '\t' '\n']+
  26 let OC    = "\\*"
  27 let CC    = "*\\"
  28 let FIG   = ['0'-'9']
  29 let ALPHA = ['A'-'Z' 'a'-'z' '_']
  30 let QT    = '"'
  31 let ID    = ALPHA+ (ALPHA | FIG)*
  32 let IX    = FIG+
  33
  34 rule block_comment = parse
  35    | CC  { () }
  36    | OC  { block_comment lexbuf; block_comment lexbuf }
  37    | _   { block_comment lexbuf }
  38 and qstring = parse
  39    | QT    { ""                                }
  40    | SPC   { " " ^ qstring lexbuf              }
  41    | BS BS { "\\" ^ qstring lexbuf             }
  42    | BS QT { "\"" ^ qstring lexbuf             }
  43    | _ as c { String.make 1 c ^ qstring lexbuf }
  44 and token = parse
  45    | SPC          { token lexbuf                                         }
  46    | OC           { block_comment lexbuf; token lexbuf                   }
  47    | ID as id     { IFDEF LEXER THEN out ("ID " ^ id) ELSE () END; TP.ID id                 }
  48    | IX as ix     { IFDEF LEXER THEN out ("IX " ^ ix) ELSE () END; TP.IX (int_of_string ix) }
  49    | QT           { let s = qstring lexbuf in
  50                     IFDEF LEXER THEN out ("STR " ^ s) ELSE () END; TP.STR s
  51                   }
  52    | "\\graph"    { IFDEF LEXER THEN out "GRAPH" ELSE () END; TP.GRAPH }
  53    | "\\main"     { IFDEF LEXER THEN out "MAIN" ELSE () END; TP.MAIN   }
  54    | "\\decl"     { IFDEF LEXER THEN out "DECL" ELSE () END; TP.DECL   }
  55    | "\\ax"       { IFDEF LEXER THEN out "AX" ELSE () END; TP.AX       }
  56    | "\\cong"     { IFDEF LEXER THEN out "CONG" ELSE () END; TP.CONG   }
  57    | "\\def"      { IFDEF LEXER THEN out "DEF" ELSE () END; TP.DEF     }
  58    | "\\th"       { IFDEF LEXER THEN out "TH" ELSE () END; TP.TH       }
  59    | "\\generate" { IFDEF LEXER THEN out "GEN" ELSE () END; TP.GEN     }
  60    | "\\require"  { IFDEF LEXER THEN out "REQ" ELSE () END; TP.REQ     }
  61    | "\\open"     { IFDEF LEXER THEN out "OPEN" ELSE () END; TP.OPEN   }
  62    | "\\close"    { IFDEF LEXER THEN out "CLOSE" ELSE () END; TP.CLOSE }
  63    | "\\sorts"    { IFDEF LEXER THEN out "SORTS" ELSE () END; TP.SORTS }
  64    | "("          { IFDEF LEXER THEN out "OP" ELSE () END; TP.OP       }
  65    | ")"          { IFDEF LEXER THEN out "CP" ELSE () END; TP.CP       }
  66    | "["          { IFDEF LEXER THEN out "OB" ELSE () END; TP.OB       }
  67    | "]"          { IFDEF LEXER THEN out "CB" ELSE () END; TP.CB       }
  68    | "{"          { IFDEF LEXER THEN out "OC" ELSE () END; TP.OC       }
  69    | "}"          { IFDEF LEXER THEN out "CC" ELSE () END; TP.CC       }
  70    | "<"          { IFDEF LEXER THEN out "OA" ELSE () END; TP.OA       }
  71    | ">"          { IFDEF LEXER THEN out "CA" ELSE () END; TP.CA       }
  72    | "."          { IFDEF LEXER THEN out "FS" ELSE () END; TP.FS       }
  73    | ":"          { IFDEF LEXER THEN out "CN" ELSE () END; TP.CN       }
  74    | ","          { IFDEF LEXER THEN out "CM" ELSE () END; TP.CM       }
  75    | "="          { IFDEF LEXER THEN out "EQ" ELSE () END; TP.EQ       }
  76    | "*"          { IFDEF LEXER THEN out "STAR" ELSE () END; TP.STAR   }
  77    | "#"          { IFDEF LEXER THEN out "HASH" ELSE () END; TP.HASH   }
  78    | "~"          { IFDEF LEXER THEN out "TE" ELSE () END; TP.TE       }
  79    | "^"          { IFDEF LEXER THEN out "CT" ELSE () END; TP.CT       }
  80    | eof          { IFDEF LEXER THEN out "EOF" ELSE () END; TP.EOF     }