helm/software/lambda-delta/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 P = TxtParser
  15
  16    let debug = false
  17    let out s = if debug then L.warn s else ()
  18 }
  19
  20 let BS    = "\\"
  21 let SPC   = [' ' '\t' '\n']+
  22 let OC    = "\\*"
  23 let CC    = "*\\"
  24 let FIG   = ['0'-'9']
  25 let ALPHA = ['A'-'Z' 'a'-'z' '_']
  26 let QT    = '"'
  27 let ID    = ALPHA+ (ALPHA | FIG)*
  28 let IX    = FIG+
  29
  30 rule block_comment = parse
  31    | CC  { () }
  32    | OC  { block_comment lexbuf; block_comment lexbuf }
  33    | _   { block_comment lexbuf }
  34 and qstring = parse
  35    | QT    { ""                                    }
  36    | SPC   { " " ^ qstring lexbuf                  }
  37    | BS BS { "\\" ^ qstring lexbuf                 }
  38    | BS QT { "\"" ^ qstring lexbuf                 }
  39    | _     { Lexing.lexeme lexbuf ^ qstring lexbuf }
  40 and token = parse
  41    | SPC       { token lexbuf                                 }
  42    | OC        { block_comment lexbuf; token lexbuf           }
  43    | ID as id  { out "ID"; P.ID id                            }
  44    | IX as ix  { out "IX"; P.IX (int_of_string ix)            }
  45    | QT        { let s = qstring lexbuf in out "STR"; P.STR s }
  46    | "\\graph" { out "GRAPH"; P.GRAPH }
  47    | "\\decl"  { out "DECL"; P.DECL   }
  48    | "\\ax"    { out "AX"; P.AX       }
  49    | "\\def"   { out "DEF"; P.DEF     }
  50    | "\\th"    { out "TH"; P.TH       }
  51    | "\\open"  { out "OPEN"; P.OPEN   }
  52    | "\\close" { out "CLOSE"; P.CLOSE }
  53    | "\\sorts" { out "SORTS"; P.SORTS }
  54    | "("       { out "OP"; P.OP       }
  55    | ")"       { out "CP"; P.CP       }
  56    | "["       { out "OB"; P.OB       }
  57    | "]"       { out "CB"; P.CB       }
  58    | "<"       { out "OA"; P.OA       }
  59    | ">"       { out "CA"; P.CA       }
  60    | "."       { out "FS"; P.FS       }
  61    | ":"       { out "CN"; P.CN       }
  62    | ","       { out "CM"; P.CM       }
  63    | "="       { out "EQ"; P.EQ       }
  64    | "*"       { out "STAR"; P.STAR   }
  65    | "#"       { out "HASH"; P.HASH   }
  66    | "+"       { out "PLUS"; P.PLUS   }
  67    | "~"       { out "TE"; P.TE       }
  68    | "->"      { out "WTO"; P.WTO     }
  69    | "=>"      { out "STO"; P.STO     }
  70    | eof       { out "EOF"; P.EOF     }