many changes:

[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 8848a3ce5045b4648e1d3f8b49fe5db27444e931..f157af40696876a7f38b65946cb6c72acc588590 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -30,6 +30,7 @@ open Printf
 exception Error of int * int * string
 
 let regexp number = xml_digit+
+let regexp utf8_blank = " " | "\n" | "\t" | [160] (* this is a nbsp *)
 
   (* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
 (* let regexp ident_letter = xml_letter *)
@@ -75,7 +76,7 @@ let regexp meta_ident = "$" ident
 let regexp meta_anonymous = "$_"
 let regexp qstring = '"' [^ '"']* '"'
 
-let regexp begincomment = "(**" xml_blank
+let regexp begincomment = "(**" utf8_blank
 let regexp beginnote = "(*"
 let regexp endcomment = "*)"
 (* let regexp comment_char = [^'*'] | '*'[^')']
@@ -123,9 +124,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 *)
@@ -228,7 +230,7 @@ let read_unparsed_group token_name lexbuf =
 
 let rec level2_meta_token =
   lexer
-  | xml_blank+ -> level2_meta_token lexbuf
+  | utf8_blank+ -> level2_meta_token lexbuf
   | ident ->
       let s = Ulexing.utf8_lexeme lexbuf in
        begin
@@ -278,8 +280,10 @@ 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)
+  | utf8_blank+ -> ligatures_token level2_ast_token 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 ->
@@ -317,7 +321,7 @@ and level2_ast_token =
 
 and level1_pattern_token =
   lexer
-  | xml_blank+ -> ligatures_token level1_pattern_token lexbuf
+  | utf8_blank+ -> ligatures_token level1_pattern_token lexbuf
   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
   | ident ->
       let s = Ulexing.utf8_lexeme lexbuf in