update in basic_2

[helm.git] / matitaB / components / content_pres / cicNotationPres.ml

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 6bcec8edd4d722062d71f986a19a3edd7e069354..553ab1ae1ba2aa352439e0935255e8318eff52d5 100644 (file)
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -87,8 +87,8 @@ let box_of spec attrs children =
            children
        in
         let attrs' =
-         (if spacing then RenderingAttrs.spacing_attributes `BoxML else [])
-          @ (if indent then RenderingAttrs.indent_attributes `BoxML else [])
+          (if spacing then [None, "spacing", "0.5em"] else [])
+          @ (if indent then [None, "indent", "0.5em"] else []) 
           @ attrs
         in
           match kind with
@@ -103,7 +103,19 @@ let render status ?(prec=(-1)) =
     | A.AttributedTerm _ ->
         aux_attributes [] ""  prec t
     | A.Num (literal, _) -> Box.Text ([], literal)
-    | A.Symbol (literal, _) -> Box.Text ([], literal)
+    | A.Symbol (literal, Some (None,desc)) ->
+        let literal = to_unicode literal in
+        let attr = [ None, "title", desc ] in
+          Box.Text (attr, literal)
+    | A.Symbol (literal, Some (Some u,desc)) -> 
+        let literal = to_unicode literal in
+        let attr = [ None, "title", desc; None, "href", u ] in
+        Box.Text (attr, literal)
+    | A.Symbol (literal, _) -> Box.Text ([], to_unicode literal)
+    | A.Ident (literal, `Uri u) ->
+        let attr = [ None, "href", u ] in
+        let literal = to_unicode literal in
+        Box.Text (attr,literal)
     | A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
     | A.Meta(n, l) ->
         let local_context =
@@ -118,7 +130,17 @@ let render status ?(prec=(-1)) =
         Box.H ([],
           (Box.Text ([], "?"^string_of_int n)::
             (if (l <> []) then [Box.H ([],local_context)] else [])))
-    | A.Literal l -> aux_literal prec l
+    | A.Literal (_,`Symbol (s,x))
+    | A.Literal (_,`Keyword (s,x))
+    | A.Literal (_,`Number (s,x)) ->
+       let attr = 
+         match x with
+         | None, None -> []
+         | Some u, None -> [ None, "href", u ]
+         | None, Some d -> [ None, "title", d ]
+         | Some u, Some d -> [ None, "href", u; None, "title", d ]
+       in        
+       Box.Text (attr, to_unicode s)
     | A.UserInput -> Box.Text ([], "%")
     | A.Layout l -> aux_layout prec l
     | A.Magic _
@@ -169,12 +191,6 @@ let render status ?(prec=(-1)) =
 (*     prerr_endline (NotationPp.pp_term t); *)
     aux_attribute t
 
-  and aux_literal prec l =
-    (match l with
-    | `Symbol s -> Box.Text ([], to_unicode s)
-    | `Keyword s -> Box.Text ([], to_unicode s)
-    | `Number s  -> Box.Text ([], to_unicode s))
-
   and aux_layout prec l =
     let attrs = [] in
     let invoke' t = aux prec t in
@@ -194,17 +210,47 @@ let render status ?(prec=(-1)) =
     | A.InfRule (t1, t2, t3) -> assert false
     | A.Sqrt t -> assert false
     | A.Root (t1, t2) -> assert false
-    | A.Box (a, terms) -> 
-        let children = List.map (aux prec) terms in
-        Box.H([],children)
+    | A.Box ((_,spacing,_) as kind, terms) ->
+        let children =
+          aux_children spacing prec
+            (NotationUtil.ungroup terms)
+        in
+        box_of kind attrs children
     | A.Mstyle (l,terms) -> assert false
     | A.Mpadded (l,terms) -> assert false
     | A.Maction alternatives -> 
          toggle_action (List.map invoke_reinit alternatives)
     | A.Group terms -> assert false 
-    | A.Break -> Box.Space [] 
+    | A.Break -> Box.Space []
+  and aux_children spacing prec 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] ->
+                aux_list false clusters
+                  (aux prec hd :: acc) []
+          | hd :: tl ->
+                aux_list false clusters
+                  (aux prec hd :: acc) tl
+      in
+        aux_list true [] []
+    in
+    let boxify_pres =
+      function
+          [t] -> t
+        | tl -> box_of (A.H, spacing, false) [] tl
+    in
+      List.map boxify_pres (find_clusters terms) 
   in
-  aux prec
+  (fun t ->
+   (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*)
+  aux prec t)
 
 (* let render_to_boxml id_to_uri t =
   let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in
@@ -221,14 +267,15 @@ let render_context_entry status name = function
               render status (TermContentPres.pp_ast status t)])
 
 let render_context status context =
-  Box.V ([],
+  Box.V ([], 
+         Box.Space [None, "width", "0.5em"]:: 
         List.map 
           (fun (name,entry) -> 
              render_context_entry status (to_unicode name) entry) context)
 
 let render_sequent status (i,context,ty) =
   Box.V ([],
-        [render_context status context;
+        [render_context status (List.rev context);
          Box.Ink [None,"width","4cm"; None,"height","2px"];
           render status (TermContentPres.pp_ast status ty)])