* added group box (?)

[helm.git] / helm / ocaml / cic_notation / cicNotationPres.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index a14ff349d8c5db23e9d9cebd83071e341f15f8c9..4b47b9014807f37596ff164727f193983e35f2d1 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -68,32 +68,33 @@ let genuine_math =
 
 let box_of mathonly spec attrs children =
   match children with
-  | [t] -> t
-  | _ ->
-      let kind, spacing, indent = spec in
-      let rec dress = function
-      | [] -> []
-      | [hd] -> [hd]
-      | hd :: tl -> hd :: Mpresentation.Mtext ([], " ") :: dress tl
-      in
-      if mathonly then Mpresentation.Mrow (attrs, dress children)
-      else
-        let attrs' =
-          if spacing then [None, "spacing", "0.5em"] else []
-          @ if indent then [None, "indent", "0em 0.5em"] else []
-          @ attrs
-        in
-        match kind with
-        | CicNotationPt.H when List.for_all genuine_math children ->
-            Mpresentation.Mrow (attrs', children)
-    | CicNotationPt.H ->
-        mpres_of_box (Box.H (attrs', List.map box_of_mpres children))
-    | CicNotationPt.V ->
-        mpres_of_box (Box.V (attrs', List.map box_of_mpres children))
-    | CicNotationPt.HV ->
-        mpres_of_box (Box.HV (attrs', List.map box_of_mpres children))
-    | CicNotationPt.HOV ->
-        mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children))
+    | [t] -> t
+    | _ ->
+       let kind, spacing, indent = spec in
+       let dress children =
+         if spacing then
+           CicNotationUtil.dress (Mpresentation.Mtext ([], " ")) children
+         else
+           children
+       in
+         if mathonly then Mpresentation.Mrow (attrs, dress children)
+         else
+            let attrs' =
+             (if spacing then [None, "spacing", "0.5em"] else [])
+               @ (if indent then [None, "indent", "0em 0.5em"] else [])
+                 @ attrs
+            in
+              match kind with
+               | CicNotationPt.H when List.for_all genuine_math children ->
+                   Mpresentation.Mrow (attrs', dress children)
+               | CicNotationPt.H ->
+                   mpres_of_box (Box.H (attrs', List.map box_of_mpres children))
+               | CicNotationPt.V ->
+                   mpres_of_box (Box.V (attrs', List.map box_of_mpres children))
+               | CicNotationPt.HV ->
+                   mpres_of_box (Box.HV (attrs', List.map box_of_mpres children))
+               | CicNotationPt.HOV ->
+                   mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children))
 
 let open_paren   = Mpresentation.Mo ([], "(")
 let closed_paren = Mpresentation.Mo ([], ")")
@@ -238,39 +239,53 @@ let render ids_to_uris =
         P.Mfrac (atop_attributes @ attrs, invoke' t1, invoke' t2)
     | A.Sqrt t -> P.Msqrt (attrs, invoke' t)
     | A.Root (t1, t2) -> P.Mroot (attrs, invoke' t1, invoke' t2)
-    | A.Box (kind, terms) ->
-        let children = aux_children mathonly xref pos prec uris terms in
+    | A.Box ((_, spacing, _) as kind, terms) ->
+        let children = aux_children mathonly spacing xref pos prec uris (CicNotationUtil.ungroup terms) in
           box_of mathonly kind attrs children
+    | A.Group terms ->
+       let children = aux_children false mathonly xref pos prec uris (CicNotationUtil.ungroup terms) in
+         box_of mathonly (A.H, false, false) attrs children
     | A.Break -> assert false (* TODO? *)
-  and aux_children mathonly xref pos prec uris terms =
-    let rec aux_list first =
+  and aux_children mathonly spacing xref pos prec uris terms =
+    let find_clusters =
+      let rec aux_list first clusters acc =
+       function
+           [] when acc = [] -> List.rev clusters
+         | [] -> aux_list first (List.rev acc :: clusters) [] []
+         | (A.Layout A.Break) :: tl when acc = [] -> aux_list first clusters [] tl
+         | (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
+               aux_list false clusters (aux [] mathonly xref pos' prec uris 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
+               aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) tl
+      in
+       aux_list true [] []
+    in
+    let boxify_pres =
       function
-        [] -> []
-      | [t] ->
-         assert (not first);
-         let pos' = 
-           match pos with
-               `None -> `Right
-             | `Inner -> `Inner
-             | `Right -> `Right
-             | `Left -> `Inner
-         in
-          [aux [] mathonly xref pos' prec uris t]
-      | t :: tl ->
-         let pos' =
-           match pos, first with
-               `None, true -> `Left
-             | `None, false -> `Inner
-             | `Left, true -> `Left
-             | `Left, false -> `Inner
-             | `Right, _ -> `Inner
-             | `Inner, _ -> `Inner
-         in
-          (aux [] mathonly xref pos' prec uris t) :: aux_list false tl
+         [t] -> t
+       | tl -> box_of mathonly (A.H, spacing, false) [] tl
     in
-      match terms with
-      | [t] -> [aux [] mathonly xref pos prec uris t]
-      | tl -> aux_list true tl
+      List.map boxify_pres (find_clusters terms)
   in
   aux [] false None `None 0 []