let debug = false
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 = ['#' '%']
| "'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 }