notation with mstyle attributes, like colors and size

[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 bbf7de133addba6e2e2cb93a60d6ffda753f56ba..4221417a0183dbf19a2e54cf140a802fdaad9ba4 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -31,6 +31,11 @@ exception Error of int * int * string
 
 let regexp number = xml_digit+
 let regexp utf8_blank = " " | "\r\n" | "\n" | "\t" | [160] (* this is a nbsp *)
+let regexp floatwithunit = 
+  [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" )
+let regexp color = "#" [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f'
+'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
+[ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
 
   (* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
 (* let regexp ident_letter = xml_letter *)
@@ -50,10 +55,10 @@ let is_ligature_char =
       true
     with Not_found -> false))
 
-let regexp we_proved = "we" ' '+ "proved"
-let regexp we_have = "we" ' '+ "have"
-let regexp let_rec = "let" ' '+ "rec" 
-let regexp let_corec = "let" ' '+  "corec"
+let regexp we_proved = "we" utf8_blank+ "proved"
+let regexp we_have = "we" utf8_blank+ "have"
+let regexp let_rec = "let" utf8_blank+ "rec" 
+let regexp let_corec = "let" utf8_blank+  "corec"
 let regexp ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident = ident_letter ident_cont* ident_decoration*
@@ -98,7 +103,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"
+    "term"; "ident"; "number"; "mstyle"
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -333,6 +338,9 @@ and level1_pattern_token =
          else
            return lexbuf ("IDENT", s)
        end
+  | color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf)
+  | floatwithunit -> 
+      return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
   | qkeyword ->
       return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))