X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=553ab1ae1ba2aa352439e0935255e8318eff52d5;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=04440ffe7a75cefe1ce1b7d9315f2ef197928611;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml
index 04440ffe7..553ab1ae1 100644
--- a/matitaB/components/content_pres/cicNotationPres.ml
+++ b/matitaB/components/content_pres/cicNotationPres.ml
@@ -23,129 +23,21 @@
  * http://helm.cs.unibo.it/
  *)
 
-(* $Id$ *)
-
 open Printf
 
-module Ast = NotationPt
-module Mpres = Mpresentation
-
-type mathml_markup = boxml_markup Mpres.mpres
-and boxml_markup = mathml_markup Box.box
+module A = NotationPt
 
-type markup = mathml_markup
-
-let atop_attributes = [None, "linethickness", "0pt"]
+type markup = string Box.box
 
 let to_unicode = Utf8Macro.unicode_of_tex
 
-let rec make_attributes l1 = function
-  | [] -> []
-  | hd :: tl ->
-      (match hd with
-      | None -> make_attributes (List.tl l1) tl
-      | Some s ->
-          let p,n = List.hd l1 in
-          (p,n,s) :: make_attributes (List.tl l1) tl)
-
-let box_of_mpres =
-  function
-  | Mpresentation.Mobject (attrs, box) ->
-      assert (attrs = []);
-      box
-  | mpres -> Box.Object ([], mpres)
-
-let mpres_of_box =
-  function
-  | Box.Object (attrs, mpres) ->
-      assert (attrs = []);
-      mpres
-  | box -> Mpresentation.Mobject ([], box)
-
-let rec genuine_math =
-  function
-  | Mpresentation.Mobject ([], obj) -> not (genuine_box obj)
-  | _ -> true
-and genuine_box =
-  function
-  | Box.Object ([], mpres) -> not (genuine_math mpres)
-  | _ -> true
-
-let rec eligible_math =
-  function
-  | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> eligible_math mpres
-  | Mpresentation.Mobject ([], _) -> false
-  | _ -> true
-
-let rec promote_to_math =
-  function
-  | Mpresentation.Mobject ([], Box.Object ([], mpres)) -> promote_to_math mpres
-  | math -> math
-
-let small_skip =
-  Mpresentation.Mspace (RenderingAttrs.small_skip_attributes `MathML)
+let small_skip    = Box.Text ([], " ")
+let open_paren    = Box.Text ([], "(")
+let closed_paren  = Box.Text ([], ")")
+let semicolon     = Box.Text ([], ";")
 
-let rec add_mpres_attributes new_attr = function
-  | Mpresentation.Mobject (attr, box) ->
-      Mpresentation.Mobject (attr, add_box_attributes new_attr box)
-  | mpres ->
-      Mpresentation.set_attr (new_attr @ Mpresentation.get_attr mpres) mpres
-and add_box_attributes new_attr = function
-  | Box.Object (attr, mpres) ->
-      Box.Object (attr, add_mpres_attributes new_attr mpres)
-  | box -> Box.set_attr (new_attr @ Box.get_attr box) box
-
-let box_of mathonly spec attrs children =
-  match children with
-    | [t] -> add_mpres_attributes attrs t
-    | _ ->
-	let kind, spacing, indent = spec in
-	let dress children =
-	  if spacing then
-	    NotationUtil.dress small_skip children
-	  else
-	    children
-	in
-	  if mathonly then Mpresentation.Mrow (attrs, dress children)
-	  else
-            let attrs' =
-	      (if spacing then RenderingAttrs.spacing_attributes `BoxML else [])
-              @ (if indent then RenderingAttrs.indent_attributes `BoxML else [])
-              @ attrs
-            in
-              match kind with
-                | Ast.H ->
-                    if List.for_all eligible_math children then
-                      Mpresentation.Mrow (attrs',
-                        dress (List.map promote_to_math children))
-                    else
-                      mpres_of_box (Box.H (attrs',
-                        List.map box_of_mpres children))
-(*                 | Ast.H when List.for_all genuine_math children ->
-                    Mpresentation.Mrow (attrs', dress children) *)
-		| Ast.V ->
-		    mpres_of_box (Box.V (attrs',
-                      List.map box_of_mpres children))
-		| Ast.HV ->
-		    mpres_of_box (Box.HV (attrs',
-                      List.map box_of_mpres children))
-		| Ast.HOV ->
-		    mpres_of_box (Box.HOV (attrs',
-                      List.map box_of_mpres children))
-
-let open_paren        = Mpresentation.Mo ([], "(")
-let closed_paren      = Mpresentation.Mo ([], ")")
-let open_bracket      = Mpresentation.Mo ([], "[")
-let closed_bracket    = Mpresentation.Mo ([], "]")
-let open_brace        = Mpresentation.Mo ([], "{")
-let closed_brace      = Mpresentation.Mo ([], "}")
-let hidden_substs     = Mpresentation.Mtext ([], "{...}")
-let hidden_lctxt      = Mpresentation.Mtext ([], "[...]")
-let open_box_paren    = Box.Text ([], "(")
-let closed_box_paren  = Box.Text ([], ")")
-let semicolon         = Mpresentation.Mo ([], ";")
 let toggle_action children =
-  Mpresentation.Maction ([None, "actiontype", "toggle"], children)
+  Box.Action ([None, "actiontype", "toggle"], children)
 
 type child_pos = [ `Left | `Right | `Inner ]
 
@@ -155,31 +47,17 @@ let pp_assoc =
   | Gramext.RightA -> "RightA"
   | Gramext.NonA -> "NonA"
 
-let is_atomic t =
-  let rec aux_mpres = function
-    | Mpres.Mi _
-    | Mpres.Mo _
-    | Mpres.Mn _
-    | Mpres.Ms _
-    | Mpres.Mtext _
-    | Mpres.Mspace _ -> true
-    | Mpres.Mobject (_, box) -> aux_box box
-    | Mpres.Maction (_, [mpres])
-    | Mpres.Mrow (_, [mpres]) -> aux_mpres mpres
-    | _ -> false
-  and aux_box = function
-    | Box.Space _
-    | Box.Ink _
-    | Box.Text _ -> true
-    | Box.Object (_, mpres) -> aux_mpres mpres
-    | Box.H (_, [box])
-    | Box.V (_, [box])
-    | Box.HV (_, [box])
-    | Box.HOV (_, [box])
-    | Box.Action (_, [box]) -> aux_box box
-    | _ -> false
-  in
-  aux_mpres t
+let rec is_atomic = function
+  | Box.Space _
+  | Box.Ink _
+  | Box.Text _ 
+  | Box.Object _ -> true
+  | Box.H (_, [box])
+  | Box.V (_, [box])
+  | Box.HV (_, [box])
+  | Box.HOV (_, [box])
+  | Box.Action (_, [box]) -> is_atomic box
+  | _ -> false
 
 let add_parens child_prec curr_prec t =
   if is_atomic t then 
@@ -191,127 +69,87 @@ let add_parens child_prec curr_prec t =
     (*prerr_endline ("adding parens around: "^
       BoxPp.render_to_string (function x::_->x|_->assert false)
         ~map_unicode_to_tex:false 80 t);*)
-    match t with
-    | Mpresentation.Mobject (_, box) ->
-        mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
-    | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
+      Box.H ([], [ open_paren; t; closed_paren ])
   end else
     ((*prerr_endline ("NOT adding parens around: "^
       BoxPp.render_to_string (function x::_->x|_->assert false)
         ~map_unicode_to_tex:false 80 t);*)t)
 
-let render status ~lookup_uri ?(prec=(-1)) =
-  let module A = Ast in
-  let module P = Mpresentation in
-(*   let use_unicode = true in *)
-  let make_href xmlattrs xref =
-    let xref_uris =
-      List.fold_right
-        (fun xref uris ->
-          match lookup_uri xref with
-          | None -> uris
-          | Some uri -> uri :: uris)
-        !xref []
-    in
-    let xmlattrs_uris, xmlattrs =
-      let xref_attrs, other_attrs =
-        List.partition
-          (function Some "xlink", "href", _ -> true | _ -> false)
-          xmlattrs
-      in
-      List.map (fun (_, _, uri) -> uri) xref_attrs,
-      other_attrs
-    in
-    let uris =
-      match xmlattrs_uris @ xref_uris with
-      | [] -> None
-      | uris ->
-          Some (String.concat " "
-            (HExtlib.list_uniq (List.sort String.compare uris)))
-    in
-    let xrefs =
-      match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs)
-    in
-    xref := [];
-    xmlattrs
-    @ make_attributes [Some "helm", "xref"; Some "xlink", "href"]
-        [xrefs; uris]
-  in
-  let make_xref xref =
-    let xrefs =
-      match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs)
-    in
-    xref := [];
-    make_attributes [Some "helm","xref"] [xrefs]
-  in
-  (* when mathonly is true no boxes should be generated, only mrows *)
-  (* "xref" is  *)
-  let rec aux xmlattrs mathonly xref  prec t =
+let box_of spec attrs children =
+  match children with
+    | [t] -> t
+    | _ ->
+	let kind, spacing, indent = spec in
+	let dress children =
+	  if spacing then
+	    NotationUtil.dress small_skip children
+	  else
+	    children
+	in
+        let attrs' =
+          (if spacing then [None, "spacing", "0.5em"] else [])
+          @ (if indent then [None, "indent", "0.5em"] else []) 
+          @ attrs
+        in
+          match kind with
+            | A.H -> Box.H (attrs',children)
+	    | A.V -> Box.V (attrs',children)
+	    | A.HV -> Box.HV (attrs',children)
+	    | A.HOV -> Box.HOV (attrs',children)
+
+let render status ?(prec=(-1)) =
+  let rec aux prec t =
     match t with
     | A.AttributedTerm _ ->
-        aux_attributes xmlattrs mathonly xref  prec t
-    | A.Num (literal, _) ->
-        let attrs =
-          (RenderingAttrs.number_attributes `MathML)
-          @ make_href xmlattrs xref
-        in
-        Mpres.Mn (attrs, literal)
-    | A.Symbol (literal, _) ->
-        let attrs =
-          (RenderingAttrs.symbol_attributes `MathML)
-          @ make_href xmlattrs xref
-        in
-        Mpres.Mo (attrs, to_unicode literal)
-    | A.Ident (literal, subst)
-    | A.Uri (literal, subst) ->
-        let attrs =
-          (RenderingAttrs.ident_attributes `MathML)
-          @ make_href xmlattrs xref
-        in
-        let name = Mpres.Mi (attrs, to_unicode literal) in
-        (match subst with
-        | Some []
-        | None -> name
-        | Some substs ->
-            let substs' =
-              box_of mathonly (A.H, false, false) []
-                (open_brace
-                :: (NotationUtil.dress semicolon
-                    (List.map
-                      (fun (name, t) ->
-                        box_of mathonly (A.H, false, false) [] [
-                          Mpres.Mi ([], name);
-                          Mpres.Mo ([], to_unicode "\\def");
-                          aux [] mathonly xref  prec t ])
-                      substs))
-                @ [ closed_brace ])
-            in
-            let substs_maction = toggle_action [ hidden_substs; substs' ] in
-            box_of mathonly (A.H, false, false) [] [ name; substs_maction ])
+        aux_attributes [] ""  prec t
+    | A.Num (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 l =
-          box_of mathonly (A.H, false, false) []
-            ([ Mpres.Mtext ([], "[") ] @ 
-            (NotationUtil.dress (Mpres.Mtext ([],  ";"))
+        let local_context =
+          Box.Text ([], "["):: 
+            (NotationUtil.dress (Box.Text ([],  ";"))
               (List.map 
                 (function 
-                | None -> Mpres.Mtext ([],  "_")
-                | Some t -> aux xmlattrs mathonly xref  prec t) l)) @
-             [ Mpres.Mtext ([], "]")])
+                | None -> Box.Text ([],  "_")
+                | Some t -> aux prec t) l)) @
+            [Box.Text ([], "]")]
         in
-        let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in
-        box_of mathonly (A.H, false, false) []
-          ([Mpres.Mtext ([], "?"^string_of_int n) ] 
-            @ (if l <> [] then [lctxt_maction] else []))
-    | A.Literal l -> aux_literal xmlattrs xref prec l
-    | A.UserInput -> Mpres.Mtext ([], "%")
-    | A.Layout l -> aux_layout mathonly xref  prec l
+        Box.H ([],
+          (Box.Text ([], "?"^string_of_int n)::
+            (if (l <> []) then [Box.H ([],local_context)] else [])))
+    | 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 _
     | A.Variable _ -> assert false  (* should have been instantiated *)
     | t ->
         prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
         assert false
-  and aux_attributes xmlattrs mathonly xref  prec t =
+
+  and aux_attributes xmlattrs xref  prec t =
     let reset = ref false in
     let inferred_level = ref None in
     let expected_level = ref None in
@@ -338,9 +176,9 @@ let render status ~lookup_uri ?(prec=(-1)) =
             | Some prec -> prec
           in
           (match !inferred_level with
-          | None -> aux !new_xmlattrs mathonly new_xref prec t
+          | None -> aux prec t
           | Some child_prec ->
-              let t' = aux !new_xmlattrs mathonly new_xref child_prec t in
+              let t' = aux child_prec t in
               (*prerr_endline 
                 ("inferred: "^string_of_int child_prec^ 
                  " exp: "^string_of_int prec ^ 
@@ -352,107 +190,93 @@ let render status ~lookup_uri ?(prec=(-1)) =
     in
 (*     prerr_endline (NotationPp.pp_term t); *)
     aux_attribute t
-  and aux_literal xmlattrs xref prec l =
-    let attrs = make_href xmlattrs xref in
-    (match l with
-    | `Symbol s -> Mpres.Mo (attrs, to_unicode s)
-    | `Keyword s -> Mpres.Mtext (attrs, to_unicode s)
-    | `Number s  -> Mpres.Mn (attrs, to_unicode s))
-  and aux_layout mathonly xref  prec l =
-    let attrs = make_xref xref in
-    let invoke' t = aux [] true (ref [])  prec t in
+
+  and aux_layout prec l =
+    let attrs = [] in
+    let invoke' t = aux prec t in
       (* use the one below to reset precedence and associativity *)
-    let invoke_reinit t = aux [] mathonly xref ~-1 t in
+    let invoke_reinit t = aux ~-1 t in
     match l with
     | A.Sup (A.Layout (A.Sub (t1,t2)), t3)
     | A.Sup (A.AttributedTerm (_,A.Layout (A.Sub (t1,t2))), t3)
-      -> Mpres.Msubsup (attrs, invoke' t1, invoke_reinit t2, invoke_reinit t3)
-    | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2)
-    | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2)
-    | A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2)
-    | A.Above (t1, t2) -> Mpres.Mover (attrs, invoke' t1, invoke_reinit t2)
+      -> assert false
+    | A.Sub (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"_");aux prec t2])
+    | A.Sup (t1, t2) -> Box.H ([],[aux prec t1;Box.Text ([],"^");aux prec t2])
+    | A.Below (t1, t2) -> assert false 
+    | A.Above (t1, t2) -> assert false
     | A.Frac (t1, t2)
-    | A.Over (t1, t2) ->
-        Mpres.Mfrac (attrs, invoke_reinit t1, invoke_reinit t2)
-    | A.Atop (t1, t2) ->
-        Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1,
-          invoke_reinit t2)
-    | A.InfRule (t1, t2, t3) ->
-      Mpres.Mstyle ([None,"mathsize","big"],
-       Mpres.Mrow (attrs,
-        [Mpres.Mfrac ([],
-           Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1),
-           Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2));
-          Mpres.Mstyle ([None,"scriptlevel","2"],
-           Mpresentation.Mspace 
-            (RenderingAttrs.small_skip_attributes `MathML));
-         Mpres.Mstyle ([None,"scriptlevel","1"],invoke_reinit t3)]))
-    | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t)
-    | A.Root (t1, t2) ->
-        Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2)
-    | A.Box ((_, spacing, _) as kind, terms) ->
+    | A.Over (t1, t2) -> assert false
+    | A.Atop (t1, t2) -> assert false
+    | A.InfRule (t1, t2, t3) -> assert false
+    | A.Sqrt t -> assert false
+    | A.Root (t1, t2) -> assert false
+    | A.Box ((_,spacing,_) as kind, terms) ->
         let children =
-          aux_children mathonly spacing xref  prec
+          aux_children spacing prec
             (NotationUtil.ungroup terms)
         in
-        box_of mathonly kind attrs children
-    | A.Mstyle (l,terms) -> 
-        Mpres.Mstyle 
-          (List.map (fun (k,v) -> None,k,v) l, 
-           box_of mathonly (A.H, false, false) attrs 
-            (aux_children mathonly false xref  prec 
-              (NotationUtil.ungroup terms)))
-    | A.Mpadded (l,terms) -> 
-        Mpres.Mpadded 
-          (List.map (fun (k,v) -> None,k,v) l, 
-           box_of mathonly (A.H, false, false) attrs 
-            (aux_children mathonly false xref  prec 
-              (NotationUtil.ungroup terms)))
+        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 ->
-	let children =
-          aux_children mathonly false xref  prec
-            (NotationUtil.ungroup terms)
-        in
-        box_of mathonly (A.H, false, false) attrs children
-    | A.Break -> assert false (* TODO? *)
-  and aux_children mathonly spacing xref  prec terms =
+    | A.Group terms -> assert false 
+    | 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 = [] ->
+        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 ->
+          | (A.Layout A.Break) :: tl ->
               aux_list first (List.rev acc :: clusters) [] tl
-	  | [hd] ->
-		aux_list false clusters
-                  (aux [] mathonly xref  prec hd :: acc) []
-	  | hd :: tl ->
-		aux_list false clusters
-                  (aux [] mathonly xref  prec hd :: acc) 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 [] []
+        aux_list true [] []
     in
     let boxify_pres =
       function
-	  [t] -> t
-	| tl -> box_of mathonly (A.H, spacing, false) [] tl
+          [t] -> t
+        | tl -> box_of (A.H, spacing, false) [] tl
     in
-      List.map boxify_pres (find_clusters terms)
+      List.map boxify_pres (find_clusters terms) 
   in
-  aux [] false (ref []) prec
-
-let rec print_box (t: boxml_markup) =
-  Box.box2xml print_mpres t
-and print_mpres (t: mathml_markup) =
-  Mpresentation.print_mpres print_box t
-
-let print_xml = print_mpres
+  (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
   Xml.add_xml_declaration xml_stream *)
 
+let render_context_entry status name = function
+  | A.Decl t -> 
+      Box.H ([],
+	     [Box.Text([],name); Box.Text([],":"); 
+	      render status (TermContentPres.pp_ast status t)])
+  | A.Def (t,ty) -> 
+      Box.H ([],
+	      [Box.Text([],name); Box.Text([],Utf8Macro.unicode_of_tex"\\def");
+	       render status (TermContentPres.pp_ast status t)])
+
+let render_context status context =
+  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 (List.rev context);
+	  Box.Ink [None,"width","4cm"; None,"height","2px"];
+          render status (TermContentPres.pp_ast status ty)])
+	  
+