X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=d724acf85d21d0cf014cf928c97bbc70b379cda6;hb=dee464f8cd331524663167659d1fad01e558d4e1;hp=27b55ebc1353e4594e0e5311f3aca72283e205f8;hpb=42680d47c033d751738fd0f84af7b45b2a91a5b8;p=helm.git

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 27b55ebc1..d724acf85 100644
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -52,11 +52,11 @@ let rec remove_level_info =
   | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t)
   | t -> t
 
-let add_xml_attrs attrs t =
-  if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t)
+let add_xml_attrs attrs t = t
+(*  if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) *)
 
-let add_keyword_attrs =
-  add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+let add_keyword_attrs t = t
+(*  add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) *)
 
 let box kind spacing indent content =
   Ast.Layout (Ast.Box ((kind, spacing, indent), content))
@@ -66,16 +66,16 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
-let space = Ast.Literal (`Symbol " ")
-let builtin_symbol s = Ast.Literal (`Symbol s)
-let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
+let space = Ast.Literal (`Symbol (" ", (None,None)))
+let builtin_symbol s = Ast.Literal (`Symbol (s,(None,None)))
+let keyword k = add_keyword_attrs (Ast.Literal (`Keyword (k,(None,None))))
 
 let number s =
-  add_xml_attrs (RenderingAttrs.number_attributes `MathML)
-    (Ast.Literal (`Number s))
+  add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
+    (Ast.Literal (`Number (s,(None,None))))
 
 let ident i =
-  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) 
+  add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
     (Ast.Ident (i,`Ambiguous))
 
 let ident_w_href href i =
@@ -86,13 +86,13 @@ let ident_w_href href i =
       add_xml_attrs [Some "xlink", "href", href] (ident i)
 
 let binder_symbol s =
-  add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
+  add_xml_attrs (* (RenderingAttrs.builtin_symbol_attributes `MathML) *) ()
     (builtin_symbol s)
 
 let xml_of_sort x = 
   let to_string x = Ast.Ident (x, `Ambiguous) in
   let identify x = 
-    add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
+    add_xml_attrs (* (RenderingAttrs.keyword_attributes `MathML) *) () (to_string x)
   in
   let lvl t = Ast.AttributedTerm (`Level 90,t) in
   match x with
@@ -317,9 +317,9 @@ class type g_status =
     method content_pres_db: db
   end
  
-class virtual status =
+class virtual status uid =
  object
-   inherit NCic.status
+   inherit NCic.status uid
    val content_pres_db = initial_db  
    method content_pres_db = content_pres_db
    method set_content_pres_db v = {< content_pres_db = v >}
@@ -337,8 +337,8 @@ let set_compiled21 status f =
  status#set_content_pres_db
   { status#content_pres_db with compiled21 = Some f }
 
-let add_idrefs =
-  List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
+(* let add_idrefs =
+  List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) *)
 
 let instantiate21 idrefs env l1 =
   let rec subst_singleton pos env =
@@ -376,10 +376,14 @@ let instantiate21 idrefs env l1 =
         [ value ]
     | Ast.Magic m -> subst_magic pos env m
     | Ast.Literal l as t ->
-        let t = add_idrefs idrefs t in
-        (match l with
-        | `Keyword k -> [ add_keyword_attrs t ]
-        | _ -> [ t ])
+       (match idrefs with
+        | [] -> [t]
+        | desc::_ ->
+            let desc = Some desc in
+            (match l with
+            | `Keyword (k,_) -> [ Ast.Literal (`Keyword (k,(None,desc))) ]
+            | `Symbol (s,_) -> [ Ast.Literal (`Symbol (s,(None,desc))) ]
+            | `Number (n,_) -> [ Ast.Literal (`Number (n,(None,desc))) ]))
     | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
     | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
   and subst_magic pos env = function
@@ -470,16 +474,24 @@ let rec pp_ast1 status term =
     | NotationEnv.DisambiguationValue _ as v -> v
   in
   let ast_env_of_env env =
+    prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env);
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
-(* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *)
+(* prerr_endline ("### pattern matching from 2 to 1 on term " ^
+ * NotationPp.pp_term status term); *)
+  let res =
   match term with
   | Ast.AttributedTerm (attrs, term') ->
       Ast.AttributedTerm (attrs, pp_ast1 status term')
   | _ ->
       (match get_compiled21 status term with
-      | None -> pp_ast0 status term (pp_ast1 status)
+      | None -> (* prerr_endline "### ramo 1"; *) 
+          pp_ast0 status term (pp_ast1 status)
       | Some (env, ctors, pid) ->
+          (* prerr_endline "### ramo 2";
+            prerr_endline ("### constructors:\n" ^ 
+           (String.concat "\n\n" (List.map (NotationPp.pp_term status) ctors)) ^
+           "\n\n### constructors end") *)
           let idrefs =
             List.flatten (List.map NotationUtil.get_idrefs ctors)
           in
@@ -489,6 +501,10 @@ let rec pp_ast1 status term =
             with Not_found -> assert false
           in
           instantiate21 idrefs (ast_env_of_env env) l1)
+  in
+  (* prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term
+   * status res);*)
+  res
 
 let load_patterns21 status t =
   set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t))