From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 2 Apr 2003 10:48:30 +0000 (+0000)
Subject: Underscore must be quted in TeX. Fixed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7f398a57e81555876212ff38c3c0d1cd821b718f;p=helm.git

Underscore must be quted in TeX. Fixed.
---

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