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 692a6a86b1f6e0a47e087e720c52d5b5cb4b0dfe..25fc01311bdbd7031269179e4958ab46ecb47f78 100644 (file)
--- 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