Underscore must be quted in TeX. Fixed.

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualLexer.mll

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index d40f09fb29ab04338e9db53611bf9e17911fbc77..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'
@@ -57,7 +62,7 @@ let conuri = baseuri "con"
 let varuri = baseuri "var"
 let indtyuri = baseuri "ind#1/" num
 let indconuri = baseuri "ind#1/" num "/" num
-let blanks = [' ' '\t' '\n' '~'] | "\\;"
+let blanks = [' ' '\t' '\n' '~' '{' '}'] | "\\;"
 rule token =
  parse
     blanks      { token lexbuf } (* skip blanks *)
@@ -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