X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=2b9bc650fcc9ec7b590e48e2ea27c25c5f0841d8;hb=33cef65313289250ea37c782c65306f7c967cd04;hp=53f0265b7ffff0a33d10cd5974bf4e9e9feef558;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 53f0265b7..2b9bc650f 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))
@@ -71,11 +71,11 @@ let builtin_symbol s = Ast.Literal (`Symbol s)
 let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
 
 let number s =
-  add_xml_attrs (RenderingAttrs.number_attributes `MathML)
+  add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
     (Ast.Literal (`Number s))
 
 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
@@ -467,7 +467,7 @@ let rec pp_ast1 status term =
         NotationEnv.OptValue (Some (pp_value v))
     | NotationEnv.ListValue vl ->
         NotationEnv.ListValue (List.map pp_value vl)
-    | NotationEnv.LocValue _ as v -> v
+    | NotationEnv.DisambiguationValue _ as v -> v
   in
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
@@ -575,7 +575,7 @@ let tail_names names env =
   in
   aux [] env
 
-let instantiate_level2 status env loc term =
+let instantiate_level2 status env (loc,uri,desc) term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
   let fresh_env = ref [] in
   let lookup_fresh_name n =
@@ -607,7 +607,7 @@ let instantiate_level2 status env loc term =
     | Ast.Num _
     | Ast.Sort _
     | Ast.UserInput -> term
-    | Ast.Symbol _ -> Ast.AttributedTerm (`Loc loc, term)
+    | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc)
 
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var
@@ -615,6 +615,10 @@ let instantiate_level2 status env loc term =
     | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
 
     | _ -> assert false
+  and aux_symbol s loc = function
+  | _, None -> Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
+  | uri, Some desc -> 
+      Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
   and aux_opt env = function
     | Some term -> Some (aux env term)
     | None -> None