X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=6d18fe83794c622d0657d2cc5558c5d0e241f0f1;hb=80f621454b98ac76c9c1086ffd5796dd3e2e2647;hp=f3953eb08f3e5a24302c142d38c93b15ac8e98a1;hpb=ac80c2cd2667de2942182ae0a98ad3dbadd7b559;p=helm.git

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index f3953eb08..6d18fe837 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -157,7 +157,7 @@ let extract_term_production status pattern =
     | Ast.Magic m -> aux_magic m
     | Ast.Variable v -> aux_variable v
     | t ->
-        prerr_endline (NotationPp.pp_term t);
+        prerr_endline (NotationPp.pp_term status t);
         assert false
   and aux_literal =
     function
@@ -208,8 +208,8 @@ let extract_term_production status pattern =
           match magic with
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
-          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -663,8 +663,10 @@ EXTEND
           in
           let rec find_arg name n = function 
             | [] ->
+                (* 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 name))
+                  (NotationPp.pp_term (new NCicPp.status) name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -814,7 +816,7 @@ class type g_status =
   method notation_parser_db: db
  end
 
-class status ~keywords:kwds =
+class status0 ~keywords:kwds =
  object
   val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
   method notation_parser_db = db
@@ -824,6 +826,12 @@ class status ~keywords:kwds =
    = fun o -> {< db = o#notation_parser_db >}
  end
 
+class virtual status ~keywords:kwds =
+ object
+  inherit NCic.status
+  inherit status0 kwds
+ end
+
 let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         (* move inside constructor XXX *)
   let add1item status (level, level1_pattern, action) =
@@ -848,7 +856,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
   let keywords = NotationUtil.keywords_of_term level1_pattern @
     status#notation_parser_db.keywords in
   let items = current_item :: status#notation_parser_db.items in 
-  let status = status#set_notation_parser_status (new status ~keywords) in
+  let status = status#set_notation_parser_status (new status0 ~keywords) in
   let status = status#set_notation_parser_db 
     {status#notation_parser_db with items = items} in
   List.fold_left add1item status items