From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 5 Sep 2005 15:28:12 +0000 (+0000)
Subject: avoid generating multiple times the same xref/href
X-Git-Tag: V_0_1_2_1~98
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a7ff7a3ce24bd14385d2295a1c77fad4b876cb8;p=helm.git

avoid generating multiple times the same xref/href
---

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index b3893d327..e8458a073 100644
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -34,12 +34,23 @@ let atop_attributes = [None, "linethickness", "0pt"]
 
 let to_unicode = Utf8Macro.unicode_of_tex
 
-let rec make_attributes l1 = function
+(* let rec make_attributes l1 = function
   | [] -> []
   | None :: tl -> make_attributes (List.tl l1) tl
   | Some s :: tl ->
       let p,n = List.hd l1 in
-      (p,n,s) :: make_attributes (List.tl l1) tl
+      prerr_endline (Printf.sprintf "make_attributes %s %s" n s);
+      (p,n,s) :: make_attributes (List.tl l1) tl *)
+let rec make_attributes l1 = function
+  | [] -> []
+  | hd :: tl ->
+      (match !hd with
+      | None -> make_attributes (List.tl l1) tl
+      | Some s ->
+          let p,n = List.hd l1 in
+          prerr_endline (Printf.sprintf "make_attributes %s %s" n s);
+          hd := None;
+          (p,n,s) :: make_attributes (List.tl l1) tl)
 
 let box_of_mpres =
   function
@@ -190,8 +201,8 @@ let render ids_to_uris =
     | Some id -> (try Some (Hashtbl.find ids_to_uris id) with Not_found -> None)
   in
   let make_href xmlattrs xref uris =
-    let xref_uri = lookup_uri xref in
-    let raw_uris = List.map UriManager.string_of_uri uris in
+    let xref_uri = lookup_uri !xref in
+    let raw_uris = List.map UriManager.string_of_uri !uris in
     let uri =
       match xref_uri, raw_uris with
       | None, [] -> None
@@ -199,11 +210,14 @@ let render ids_to_uris =
       | None, raw_uris -> Some (String.concat " " raw_uris)
       | Some uri, raw_uris -> Some (String.concat " " (uri :: raw_uris))
     in
+    uris := [];
     xmlattrs
-    @ make_attributes [Some "helm", "xref"; Some "xlink", "href"] [xref; uri]
+    @ make_attributes [Some "helm", "xref"; Some "xlink", "href"]
+        [xref; ref uri]
   in
   let make_xref xref = make_attributes [Some "helm","xref"] [xref] in
   (* when mathonly is true no boxes should be generated, only mrows *)
+  (* "xref" is  *)
   let rec aux xmlattrs mathonly xref pos prec uris t =
     match t with
     | A.AttributedTerm _ ->
@@ -224,7 +238,7 @@ let render ids_to_uris =
     | A.Uri (literal, subst) ->
         let attrs =
           (RenderingAttrs.ident_attributes `MathML)
-          @ make_href xmlattrs xref []
+          @ make_href xmlattrs xref (ref [])
         in
         let name = P.Mi (attrs, to_unicode literal) in
         (match subst with
@@ -284,10 +298,10 @@ let render ids_to_uris =
           aux_attribute t
       | t ->
           (match !new_level with
-          | None -> aux !new_xmlattrs mathonly !new_xref pos prec !new_uris t
+          | None -> aux !new_xmlattrs mathonly new_xref pos prec new_uris t
           | Some (child_prec, child_assoc) ->
               let t' = 
-                aux !new_xmlattrs mathonly !new_xref pos child_prec !new_uris t
+                aux !new_xmlattrs mathonly new_xref pos child_prec new_uris t
               in
               add_parens child_prec child_assoc pos prec t')
     in
@@ -309,7 +323,7 @@ let render ids_to_uris =
     | `Number s  -> P.Mn (attrs, to_unicode s))
   and aux_layout mathonly xref pos prec uris l =
     let attrs = make_xref xref in
-    let invoke' t = aux [] true None pos prec uris t in
+    let invoke' t = aux [] true (ref None) pos prec uris t in
     match l with
     | A.Sub (t1, t2) -> P.Msub (attrs, invoke' t1, invoke' t2)
     | A.Sup (t1, t2) -> P.Msup (attrs, invoke' t1, invoke' t2)
@@ -379,7 +393,7 @@ let render ids_to_uris =
     in
       List.map boxify_pres (find_clusters terms)
   in
-  aux [] false None `None 0 []
+  aux [] false (ref None) `None 0 (ref [])
 
 let rec print_box (t: boxml_markup) =
   Box.box2xml print_mpres t
diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index dba599fc8..28edd491c 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -87,7 +87,8 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
-let reset_href t = Ast.AttributedTerm (`Href [], t)
+(* let reset_href t = Ast.AttributedTerm (`Href [], t) *)
+let reset_href t = t
 let builtin_symbol s = reset_href (Ast.Literal (`Symbol s))
 let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k)))
 let number s =