X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=e34b690d311a37f16e76891c0fc6a8950d6d8d5f;hb=237f4bfbb6d79b38e9417b776495b068b54aff6a;hp=7361bf59993f7394d31fbb5c4ba7f19c4d46c834;hpb=1b67bd4dfa12ef25b8fa63884c71893b961db27d;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 7361bf599..e34b690d3 100644
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -103,7 +103,7 @@ let add_symbol_to_grammar_explicit level2_ast_grammar
           (Gramext.action (fun _ loc -> None, loc))
         ; [Gramext.Stoken ("ATAG","")
           ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
-          ;Gramext.Stoken ("SYMBOL",">")
+          ;Gramext.Stoken ("SYMBOL","\005")
           ;Gramext.Stoken ("SYMBOL",s)
           ;Gramext.Stoken ("ATAGEND","")],
           (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
@@ -321,9 +321,9 @@ let extract_term_production status pattern =
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
           | Ast.List0 (_, Some l) -> 
-              Gramext.Slist0sep (s, gram_of_literal status l)
+              Gramext.Slist0sep (s, gram_of_literal status l, true)
           | Ast.List1 (_, Some l) -> 
-              Gramext.Slist1sep (s, gram_of_literal status l)
+              Gramext.Slist1sep (s, gram_of_literal status l, true)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -724,10 +724,24 @@ EXTEND
          let uri,_ = CicNotationLexer.LocalizeEnv.find loc 
            !loctable in
          match uri with
-         | Some u -> id, `Uri u
-         | None -> id, `Ambiguous
+         | Some u -> 
+            prerr_endline ("trovata interpretazione per " ^ id ^ ": " ^ u);
+                         id, `Uri u
+         | None ->
+            prerr_endline ("identificatore ambiguo: " ^ id);
+                         id, `Ambiguous
        with
-       | Not_found -> id, `Ambiguous ]];
+       | Not_found -> 
+            prerr_endline ("identificatore non trovato: " ^ id);
+                       id, `Ambiguous ]];
+  gnum: [
+    [ n = NUMBER ->
+       try
+         match CicNotationLexer.LocalizeEnv.find loc !loctable with
+         | _uri, Some interpr -> n, Some (Some "cic:/fakeuri.def(1)",interpr)
+         | _ -> n,None 
+       with
+       | Not_found -> n,None ]];
   arg: [
     [ LPAREN; names = LIST1 gident SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN ->
@@ -782,7 +796,7 @@ EXTEND
                 (* CSC: new NCicPp.status is the best I can do here
                    without changing the return type *)
                 Ast.fail loc (sprintf "Argument %s not found"
-                  (NotationPp.pp_term (new NCicPp.status) name))
+                  (NotationPp.pp_term (new NCicPp.status None) name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -866,7 +880,7 @@ EXTEND
       | u = URI -> return_term loc (Ast.Ident 
                      (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
-      | n = NUMBER -> return_term loc (Ast.Num (n, None))
+      | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr))
       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
       | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
@@ -961,9 +975,9 @@ class status0 ~keywords:kwds =
     db.loctable := CicNotationLexer.LocalizeEnv.empty
  end
 
-class virtual status ~keywords:kwds =
+class virtual status uid ~keywords:kwds =
  object
-  inherit NCic.status
+  inherit NCic.status uid
   inherit status0 kwds
  end