Matitaweb:

[helm.git] / matitaB / components / content_pres / cicNotationParser.ml

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index fcd209307fd73e6c1202e3439a6791ef968d24c2..66037155292c62d75ca540971d7af292daee07eb 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -63,7 +63,7 @@ let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term
  ~refresh_uri_in_reference t, n)
 
 type binding =
-  | NoBinding
+  | NoBinding of string option (* name of Ast.Symbol associated to this literal *)
   | Binding of string * Env.value_type
   | Env of (string * Env.value_type) list
 
@@ -189,16 +189,17 @@ let make_action status action bindings =
   let rec aux (vl : NotationEnv.t) =
     function
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
-    | NoBinding :: tl -> 
+    | NoBinding csym :: tl -> 
         Gramext.action 
          (fun ((*_,*)(loc: Ast.location)) ->
            let uri,desc = 
              try
+               let a,b = HExtlib.loc_of_floc loc in
                CicNotationLexer.LocalizeEnv.find loc
                  !(status#notation_parser_db.loctable)
              with Not_found -> None, None
            in aux (("",(Env.NoType,
-               Env.DisambiguationValue (loc,uri,desc)))::vl) tl)
+               Env.DisambiguationValue (csym,loc,uri,desc)))::vl) tl)
     (* LUCA: DEFCON 3 BEGIN *)
     | Binding (name, Env.TermType l) :: tl ->
         Gramext.action
@@ -231,7 +232,7 @@ let flatten_opt =
   let rec aux acc =
     function
       [] -> List.rev acc
-    | NoBinding :: tl -> aux acc tl
+    | NoBinding _ :: tl -> aux acc tl
     | Env names :: tl -> aux (List.rev names @ acc) tl
     | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
   in
@@ -250,12 +251,12 @@ let update_sym_grammar status pattern =
         assert false
   and aux_literal status =
     function
-    | `Symbol (s,_) -> add_item_to_grammar status (`Sym s)
-    | `Keyword (s,_) ->  
+    | _,`Symbol (s,_) -> add_item_to_grammar status (`Sym s)
+    | _,`Keyword (s,_) ->  
          if not (List.mem s CicNotationLexer.initial_keywords)
             then add_item_to_grammar status (`Kwd s)
             else status
-    | `Number _ -> status
+    | _,`Number _ -> status
   and aux_layout status = function
     | Ast.Sub (p1, p2) -> aux (aux status p1) p2
     | Ast.Sup (p1, p2) -> aux (aux status p1) p2
@@ -279,7 +280,7 @@ let update_sym_grammar status pattern =
     | Ast.List0 (p, s)
     | Ast.List1 (p, s) ->
         let status = 
-          match s with None -> status | Some s' -> aux_literal status s'
+          match s with None -> status | Some s' -> aux_literal status (None,s')
         in
         aux status p
     | _ -> assert false
@@ -300,24 +301,24 @@ let extract_term_production status pattern =
         assert false
   and aux_literal =
     function
-    | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
-    | `Keyword (s,_) ->
+    | csym,`Symbol (s,_) -> [NoBinding csym, gram_symbol status s]
+    | csym,`Keyword (s,_) ->
         (* assumption: s will be registered as a keyword with the lexer *)
-        [NoBinding, gram_keyword status s]
-    | `Number (s,_) -> [NoBinding, gram_number s]
+        [NoBinding csym, gram_keyword status s]
+    | csym,`Number (s,_) -> [NoBinding csym, gram_number s]
   and aux_layout = function
-    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
-    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
-    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2
-    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2
-    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2
-    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
-    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2
-    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2
+    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sub "] @ aux p2
+    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sup "] @ aux p2
+    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\below "] @ aux p2
+    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\above "] @ aux p2
+    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\frac "] @ aux p2
+    | Ast.InfRule (p1, p2, p3) -> [NoBinding None, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\atop "] @ aux p2
+    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\over "] @ aux p2
     | Ast.Root (p1, p2) ->
-        [NoBinding, gram_symbol status "\\root "] @ aux p2
-        @ [NoBinding, gram_symbol status "\\of "] @ aux p1
-    | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p
+        [NoBinding None, gram_symbol status "\\root "] @ aux p2
+        @ [NoBinding None, gram_symbol status "\\of "] @ aux p1
+    | Ast.Sqrt p -> [NoBinding None, gram_symbol status "\\sqrt "] @ aux p
     | Ast.Break -> []
     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
     | Ast.Group pl -> List.flatten (List.map aux pl)
@@ -560,6 +561,14 @@ EXTEND
     | n = NUMBER -> `Number (n,(None,None))
     ]
   ];
+  rliteral: [
+    [ csymname = OPT [ "ref" ; csymname = CSYMBOL -> 
+        prerr_endline ("parser in rliteral (ref " ^ csymname ^ ")");
+        csymname ];
+      lit = literal -> 
+      csymname, lit
+    ]
+  ];
   sep:       [ [ "sep";      sep = literal -> sep ] ];
   l1_magic_pattern: [
     [ "list0"; p = l1_simple_pattern; sep = OPT sep -> 
@@ -649,7 +658,7 @@ EXTEND
              return_term_of_level loc (fun l -> Ast.Magic (m l))
       | v = l1_pattern_variable -> 
              return_term_of_level loc (fun _ -> Ast.Variable v)
-      | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
+      | l = rliteral -> return_term_of_level loc (fun _ -> Ast.Literal l)
       ]
     ];
   END