X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=d86a3124d67608b9791c0b122eaa3cf2e1c0cf92;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=21031d002fc10fba43eb915623f054d45743ecd0;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/content_pres/cicNotationLexer.ml b/matita/components/content_pres/cicNotationLexer.ml
index 21031d002..d86a3124d 100644
--- a/matita/components/content_pres/cicNotationLexer.ml
+++ b/matita/components/content_pres/cicNotationLexer.ml
@@ -29,6 +29,9 @@ open Printf
 
 exception Error of int * int * string
 
+module StringSet = Set.Make(String)
+
+(* Lexer *)
 let regexp number = xml_digit+
 let regexp utf8_blank = " " | "\r\n" | "\n" | "\t" | [160] (* this is a nbsp *)
 let regexp percentage = 
@@ -52,8 +55,6 @@ 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 nlet_rec = "nlet" utf8_blank+ "rec" 
-let regexp nlet_corec = "nlet" utf8_blank+  "corec"
 let regexp ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident_start = ident_letter 
@@ -113,22 +114,6 @@ let level2_meta_keywords =
     "anonymous"; "ident"; "number"; "term"; "fresh"
   ]
 
-  (* (string, unit) Hashtbl.t, to exploit multiple bindings *)
-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 _ = 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
@@ -152,13 +137,14 @@ let regexp uri =
 let regexp nreference =
   "cic:/"                             (* schema *)
   uri_step ('/' uri_step)*            (* path *)
-  '.'
+  '#'
   ( "dec"
-  | "def" "(" number ")"
-  | "fix" "(" number "," number "," number ")"
-  | "cfx" "(" number ")"
-  | "ind" "(" number "," number "," number ")"
-  | "con" "(" number "," number "," number ")") (* ext + reference *)
+  | "def" ":" number ""
+  | "fix" ":" number ":" number ":" number
+  | "cfx" ":" number
+  | "ind" ":" number ":" number ":" number
+  | "con" ":" number ":" number ":" number
+  ) (* ext + reference *)
 
 let error lexbuf msg =
   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
@@ -288,7 +274,7 @@ let rec comment_token acc depth =
       comment_token acc depth lexbuf
 
   (** @param k continuation to be invoked when no ligature has been found *)
-let rec ligatures_token k =
+let ligatures_token k =
   lexer
   | ligature ->
       let lexeme = Ulexing.utf8_lexeme lexbuf in
@@ -303,23 +289,21 @@ let rec ligatures_token k =
       Ulexing.rollback lexbuf;
       k lexbuf
 
-and level2_ast_token =
+let rec level2_ast_token status =
   lexer
   | let_rec -> return lexbuf ("LETREC","")
   | let_corec -> return lexbuf ("LETCOREC","")
-  | nlet_rec -> return lexbuf ("NLETREC","")
-  | nlet_corec -> return lexbuf ("NLETCOREC","")
   | we_proved -> return lexbuf ("WEPROVED","")
   | we_have -> return lexbuf ("WEHAVE","")
-  | utf8_blank+ -> ligatures_token level2_ast_token lexbuf
+  | utf8_blank+ -> ligatures_token (level2_ast_token status) 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 -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "IDENT"
+  | ident -> handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
-  | pident -> handle_keywords lexbuf (Hashtbl.mem !level2_ast_keywords) "PIDENT"
+  | pident -> handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT"
   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
   | nreference -> return lexbuf ("NREF", Ulexing.utf8_lexeme lexbuf)
@@ -342,7 +326,7 @@ and level2_ast_token =
         Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
       in
       return lexbuf ("NOTE", comment) *)
-      ligatures_token level2_ast_token lexbuf
+      ligatures_token (level2_ast_token status) lexbuf
   | begincomment -> return lexbuf ("BEGINCOMMENT","")
   | endcomment -> return lexbuf ("ENDCOMMENT","")
   | eof -> return_eoi lexbuf
@@ -369,44 +353,26 @@ and level1_pattern_token =
   | _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf)
 
 let level1_pattern_token = ligatures_token level1_pattern_token
-let level2_ast_token = ligatures_token level2_ast_token
+let level2_ast_token status = ligatures_token (level2_ast_token status)
 
 (* API implementation *)
-
-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
+type lexers = {
+        level1_pattern_lexer : (string * string) Token.glexer;
+        level2_ast_lexer : (string * string) Token.glexer;
+        level2_meta_lexer : (string * string) Token.glexer
+}
+
+let mk_lexers keywords = 
+  let initial_keywords = 
+   [ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
+   "with"; "in"; "and"; "to"; "as"; "on"; "return"; "done" ]
+  in
+  let status = 
+    List.fold_right StringSet.add (initial_keywords @ keywords) StringSet.empty 
+  in 
+  {
+        level1_pattern_lexer = mk_lexer level1_pattern_token;
+        level2_ast_lexer = mk_lexer (level2_ast_token status);
+        level2_meta_lexer = mk_lexer level2_meta_token
+  }
 ;;
-