X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcontent_pres%2FcicNotationLexer.ml;h=749731bdafcf9038923c213757f652b896c0d56c;hb=3c14f9280a8a843b3caefe67df27272f9afe0a81;hp=8848a3ce5045b4648e1d3f8b49fe5db27444e931;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/content_pres/cicNotationLexer.ml b/components/content_pres/cicNotationLexer.ml
index 8848a3ce5..749731bda 100644
--- a/components/content_pres/cicNotationLexer.ml
+++ b/components/content_pres/cicNotationLexer.ml
@@ -123,9 +123,10 @@ let _ =
     [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
       ("<=", <:unicode<leq>>);  (">=", <:unicode<geq>>);
       ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
+      ("==", <:unicode<equiv>>);
     ]
 
-let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
 
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
@@ -279,7 +280,9 @@ let rec ligatures_token k =
 and level2_ast_token =
   lexer
   | xml_blank+ -> ligatures_token level2_ast_token lexbuf
-  | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
+  | meta ->
+     let s = Ulexing.utf8_lexeme lexbuf in
+      return lexbuf ("META", String.sub s 1 (String.length s - 1))
   | implicit -> return lexbuf ("IMPLICIT", "")
   | placeholder -> return lexbuf ("PLACEHOLDER", "")
   | ident ->