From 7f398a57e81555876212ff38c3c0d1cd821b718f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 2 Apr 2003 10:48:30 +0000 Subject: [PATCH] Underscore must be quted in TeX. Fixed. --- .../texCicTextualLexer.mll | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll index 692a6a86b..25fc01311 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll @@ -47,6 +47,11 @@ (String.sub uri index_con (String.length uri - index_con)) ) ;; + + (* TeX unquoting for "_" *) + let unquote str = + Str.global_replace (Str.regexp "\\\\_") "_" str + ;; } let dollar = '$' let num = ['1'-'9']['0'-'9']* | '0' @@ -67,11 +72,15 @@ rule token = | "\\Set" { SET } | "\\Prop" { PROP } | "\\Type" { TYPE } - | ident { ID (L.lexeme lexbuf) } - | conuri { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } - | varuri { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } - | indtyuri { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) } - | indconuri { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) } + | ident { ID (unquote (L.lexeme lexbuf)) } + | conuri { CONURI + (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) } + | varuri { VARURI + (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) } + | indtyuri { INDTYURI + (indtyuri_of_uri ("cic:" ^ (unquote (L.lexeme lexbuf)))) } + | indconuri { INDCONURI + (indconuri_of_uri("cic:" ^ (unquote (L.lexeme lexbuf)))) } | num { NUM (int_of_string (L.lexeme lexbuf)) } | '?' num { let lexeme = L.lexeme lexbuf in META -- 2.39.2