X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=bbc901dab7db3e2f139e37e6e65639efe1d2abd4;hb=8c0ccf03dbefd83818bc3b6849634f422f8ec727;hp=4221417a0183dbf19a2e54cf140a802fdaad9ba4;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 4221417a0..bbc901dab 100644
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -31,8 +31,10 @@ 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 percentage = 
+  ('-' | "") [ '0' - '9' ] + '%'
 let regexp floatwithunit = 
-  [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" )
+  ('-' | "") [ '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' ]
@@ -46,15 +48,6 @@ let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ]
 let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ]
 let regexp ligature = ligature_char ligature_char+
 
-let is_ligature_char =
-  (* must be in sync with "regexp ligature_char" above *)
-  let chars = "'`~!?@*()[]<>-+=|:;.,/\"" in
-  (fun char ->
-    (try
-      ignore (String.index chars char);
-      true
-    with Not_found -> false))
-
 let regexp we_proved = "we" utf8_blank+ "proved"
 let regexp we_have = "we" utf8_blank+ "have"
 let regexp let_rec = "let" utf8_blank+ "rec" 
@@ -103,11 +96,11 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"; "mstyle"
+    "term"; "ident"; "number"; "mstyle" ; "mpadded"
   ] @ level1_layouts
 
 let level2_meta_keywords =
-  [ "if"; "then"; "else";
+  [ "if"; "then"; "elCicNotationParser.se";
     "fold"; "left"; "right"; "rec";
     "fail";
     "default";
@@ -115,18 +108,25 @@ let level2_meta_keywords =
   ]
 
   (* (string, unit) Hashtbl.t, to exploit multiple bindings *)
-let level2_ast_keywords = Hashtbl.create 23
-let _ =
-  List.iter (fun k -> Hashtbl.add level2_ast_keywords k ())
+let initial_level2_ast_keywords () = Hashtbl.create 23;;
+
+let level2_ast_keywords = ref (initial_level2_ast_keywords ())
+
+let initialize_keywords () =
+  List.iter (fun k -> Hashtbl.add !level2_ast_keywords k ())
   [ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
   "with"; "in"; "and"; "to"; "as"; "on"; "return"; "done" ]
+;;
 
-let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k ()
-let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k
+let _ = initialize_keywords ();;
+
+let add_level2_ast_keyword k = Hashtbl.add !level2_ast_keywords k ()
+let remove_level2_ast_keyword k = Hashtbl.remove !level2_ast_keywords k
 
   (* (string, int) Hashtbl.t, with multiple bindings.
    * int is the unicode codepoint *)
 let ligatures = Hashtbl.create 23
+
 let _ =
   List.iter
     (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
@@ -295,7 +295,7 @@ and level2_ast_token =
   | placeholder -> return lexbuf ("PLACEHOLDER", "")
   | ident ->
       let lexeme = Ulexing.utf8_lexeme lexbuf in
-      if Hashtbl.mem level2_ast_keywords lexeme then
+      if Hashtbl.mem !level2_ast_keywords lexeme then
         return lexbuf ("", lexeme)
       else
         return lexbuf ("IDENT", lexeme)
@@ -339,6 +339,8 @@ and level1_pattern_token =
 	    return lexbuf ("IDENT", s)
 	end
   | color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf)
+  | percentage -> 
+      return lexbuf ("PERCENTAGE", Ulexing.utf8_lexeme lexbuf)
   | floatwithunit -> 
       return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
@@ -354,14 +356,40 @@ let level2_ast_token = ligatures_token level2_ast_token
 
 (* API implementation *)
 
-let level1_pattern_lexer = mk_lexer level1_pattern_token
-let level2_ast_lexer = mk_lexer level2_ast_token
-let level2_meta_lexer = mk_lexer level2_meta_token
-
-let lookup_ligatures lexeme =
-  try
-    if lexeme.[0] = '\\'
-    then [ Utf8Macro.expand (String.sub lexeme 1 (String.length lexeme - 1)) ]
-    else List.rev (Hashtbl.find_all ligatures lexeme)
-  with Invalid_argument _ | Utf8Macro.Macro_not_found _ -> []
+let initial_level1_pattern_lexer () = mk_lexer level1_pattern_token
+let initial_level2_ast_lexer () = mk_lexer level2_ast_token
+let initial_level2_meta_lexer () = mk_lexer level2_meta_token
+
+
+let level1_pattern_lexer_ref = ref (initial_level1_pattern_lexer ())
+let level2_ast_lexer_ref = ref (initial_level2_ast_lexer ())
+let level2_meta_lexer_ref = ref (initial_level2_meta_lexer ())
+
+let level1_pattern_lexer () = !level1_pattern_lexer_ref
+let level2_ast_lexer () = !level2_ast_lexer_ref
+let level2_meta_lexer () = !level2_meta_lexer_ref 
+
+let history = ref [];;
+
+let push () =
+  history :=
+    (!level2_ast_keywords,!level1_pattern_lexer_ref,
+     !level2_ast_lexer_ref,!level2_meta_lexer_ref) :: !history;
+  level2_ast_keywords := initial_level2_ast_keywords ();
+  initialize_keywords ();
+  level1_pattern_lexer_ref := initial_level1_pattern_lexer ();
+  level2_ast_lexer_ref := initial_level2_ast_lexer ();
+  level2_meta_lexer_ref := initial_level2_meta_lexer ();
+;;
+
+let pop () =
+  match !history with
+  | [] -> assert false
+  | (kwd,pl,al,ml) :: tl -> 
+      level2_ast_keywords := kwd;
+      level1_pattern_lexer_ref := pl;
+      level2_ast_lexer_ref := al;
+      level2_meta_lexer_ref := ml;
+      history := tl
+;;