]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPres.ml
changed precedence/associativeness handling: relative position of children wrt its...
[helm.git] / helm / ocaml / cic_notation / cicNotationPres.ml
index f838521b231333ededbac6cd0f5feaba502335d3..bed2cdd4d1296638be09f7380c43d1cc41543d32 100644 (file)
@@ -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 _
@@ -304,6 +297,7 @@ let render ids_to_uris =
     let new_level = ref None in
     let new_xref = ref [] in
     let new_xmlattrs = ref [] in
+    let new_pos = ref pos in
     let rec aux_attribute =
       function
       | A.AttributedTerm (attr, t) ->
@@ -313,16 +307,17 @@ let render ids_to_uris =
           | `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')
+              add_parens child_prec child_assoc !new_pos prec t')
     in
     aux_attribute t
   and aux_literal xmlattrs xref prec l =
@@ -374,30 +369,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