X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPres.ml;h=cc3a204a4e3874ba3ee55ccb3477932ae66447bc;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=34c4c652002e15865e34f892c781a557a1148a9b;hpb=3065dd135001f868c677ee181d8a1fa3d498866a;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index 34c4c6520..cc3a204a4 100644
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -140,7 +140,7 @@ let semicolon         = Mpresentation.Mo ([], ";")
 let toggle_action children =
   Mpresentation.Maction ([None, "actiontype", "toggle"], children)
 
-type child_pos = [ `None | `Left | `Right | `Inner ]
+type child_pos = [ `Left | `Right | `Inner ]
 
 let pp_assoc =
   function
@@ -148,13 +148,6 @@ let pp_assoc =
   | Gramext.RightA -> "RightA"
   | Gramext.NonA -> "NonA"
 
-let pp_pos =
-  function
-      `None -> "`None"
-    | `Left -> "`Left"
-    | `Right -> "`Right"
-    | `Inner -> "`Inner"
-
 let is_atomic t =
   let rec aux_mpres = function
     | Mpres.Mi _
@@ -183,14 +176,19 @@ let is_atomic t =
 
 let add_parens child_prec child_assoc child_pos curr_prec t =
   if is_atomic t then t
-  else if child_prec < curr_prec
-    || (child_prec = curr_prec &&
-        child_assoc = Gramext.LeftA &&
-        child_pos <> `Left)
-    || (child_prec = curr_prec &&
-        child_assoc = Gramext.RightA &&
-        child_pos <> `Right)
+  else if child_prec >= 0
+    && (child_prec < curr_prec
+      || (child_prec = curr_prec &&
+          child_assoc = Gramext.LeftA &&
+          child_pos = `Right)
+      || (child_prec = curr_prec &&
+          child_assoc = Gramext.RightA &&
+          child_pos = `Left))
   then  (* parens should be added *)
+(*     (prerr_endline "adding parens";
+    prerr_endline (Printf.sprintf "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d"
+      child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos
+      child_pos) curr_prec); *)
     match t with
     | Mpresentation.Mobject (_, box) ->
         mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
@@ -205,7 +203,7 @@ let render ids_to_uris =
   let lookup_uri id =
     (try
       let uri = Hashtbl.find ids_to_uris id in
-      Some uri
+      Some (UriManager.string_of_uri uri)
     with Not_found -> None)
   in
   let make_href xmlattrs xref =
@@ -301,28 +299,34 @@ let render ids_to_uris =
         prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t);
         assert false
   and aux_attributes xmlattrs mathonly xref pos prec t =
+    let reset = ref false in
     let new_level = ref None in
     let new_xref = ref [] in
     let new_xmlattrs = ref [] in
+    let new_pos = ref pos in
+    let reinit = ref false in
     let rec aux_attribute =
       function
       | A.AttributedTerm (attr, t) ->
           (match attr with
           | `Loc _
           | `Raw _ -> ()
+          | `Level (-1, _) -> reset := true
           | `Level (child_prec, child_assoc) ->
               new_level := Some (child_prec, child_assoc)
           | `IdRef xref -> new_xref := xref :: !new_xref
+          | `ChildPos pos -> new_pos := pos
           | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
           aux_attribute t
       | t ->
           (match !new_level with
-          | None -> aux !new_xmlattrs mathonly new_xref pos prec t
+          | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
           | Some (child_prec, child_assoc) ->
               let t' = 
-                aux !new_xmlattrs mathonly new_xref pos child_prec t
+                aux !new_xmlattrs mathonly new_xref !new_pos child_prec t
               in
-              add_parens child_prec child_assoc pos prec t')
+              if !reset then t'
+              else add_parens child_prec child_assoc !new_pos prec t')
     in
     aux_attribute t
   and aux_literal xmlattrs xref prec l =
@@ -335,7 +339,7 @@ let render ids_to_uris =
     let attrs = make_xref xref in
     let invoke' t = aux [] true (ref []) pos prec t in
       (* use the one below to reset precedence and associativity *)
-    let invoke_reinit t = aux [] true (ref []) `None 0 t in
+    let invoke_reinit t = aux [] mathonly xref `Inner ~-1 t in
     match l with
     | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2)
     | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2)
@@ -374,30 +378,30 @@ let render ids_to_uris =
 	  | (A.Layout A.Break) :: tl ->
               aux_list first (List.rev acc :: clusters) [] tl
 	  | [hd] ->
-	      let pos' = 
-		if first then
-		  pos
-		else
-		  match pos with
-		      `None -> `Right
-		    | `Inner -> `Inner
-		    | `Right -> `Right
-		    | `Left -> `Inner
-	      in
+(*               let pos' = 
+                if first then
+                  pos
+                else
+                  match pos with
+                      `None -> `Right
+                    | `Inner -> `Inner
+                    | `Right -> `Right
+                    | `Left -> `Inner
+              in *)
 		aux_list false clusters
-                  (aux [] mathonly xref pos' prec hd :: acc) []
+                  (aux [] mathonly xref pos prec hd :: acc) []
 	  | hd :: tl ->
-	      let pos' =
-		match pos, first with
-		    `None, true -> `Left
-		  | `None, false -> `Inner
-		  | `Left, true -> `Left
-		  | `Left, false -> `Inner
-		  | `Right, _ -> `Inner
-		  | `Inner, _ -> `Inner
-	      in
+(*               let pos' =
+                match pos, first with
+                    `None, true -> `Left
+                  | `None, false -> `Inner
+                  | `Left, true -> `Left
+                  | `Left, false -> `Inner
+                  | `Right, _ -> `Inner
+                  | `Inner, _ -> `Inner
+              in *)
 		aux_list false clusters
-                  (aux [] mathonly xref pos' prec hd :: acc) tl
+                  (aux [] mathonly xref pos prec hd :: acc) tl
       in
 	aux_list true [] []
     in
@@ -408,7 +412,7 @@ let render ids_to_uris =
     in
       List.map boxify_pres (find_clusters terms)
   in
-  aux [] false (ref []) `None 0
+  aux [] false (ref []) `Inner ~-1
 
 let rec print_box (t: boxml_markup) =
   Box.box2xml print_mpres t