X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPres.ml;h=cc3a204a4e3874ba3ee55ccb3477932ae66447bc;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=bed2cdd4d1296638be09f7380c43d1cc41543d32;hpb=dfdff98e4417bae54fcf31d49c8a4d718c4487c2;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index bed2cdd4d..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
@@ -176,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 ]))
@@ -294,16 +299,19 @@ 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
@@ -317,7 +325,8 @@ let render ids_to_uris =
               let t' = 
                 aux !new_xmlattrs mathonly new_xref !new_pos child_prec t
               in
-              add_parens child_prec child_assoc !new_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 =
@@ -330,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)
@@ -403,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