-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
+(*
+ ||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 P = AutParser
let debug = false
- let out s = if debug then print_endline s else ()
+ let out s = if debug then L.warn s else ()
+
+ let unquote = ref false
+
+(* 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 = ['#' '%']
| NL { () }
| OC { block_comment lexbuf; line_comment lexbuf }
| _ { line_comment lexbuf }
- | eof { () }
+ | eof { () }
and block_comment = parse
| CC { () }
| OC { block_comment lexbuf; block_comment lexbuf }
| LC { line_comment lexbuf; block_comment lexbuf }
| _ { block_comment lexbuf }
- | eof { () }
and token = parse
| SPC { token lexbuf }
| LC { line_comment lexbuf; token lexbuf }
| "'prop'" { out "PROP"; P.PROP }
| "TYPE" { out "TYPE"; P.TYPE }
| "'type'" { out "TYPE"; P.TYPE }
- | ID { out "ID"; P.IDENT (Lexing.lexeme lexbuf) }
+ | ID { out "ID";
+ let s = Lexing.lexeme lexbuf in
+ if !unquote then P.IDENT s else P.IDENT (quote s)
+ }
| ":=" { out "DEF"; P.DEF }
| "(" { out "OP"; P.OP }
| ")" { out "CP"; P.CP }