X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationPres.ml;h=82a326c48bbb4ffc70d64400ef043b1b74955fa0;hb=HEAD;hp=84eaaeb2a7711dd85e7d898294de6729f9a5913c;hpb=8c4659819a1c1f2e450d9a588ecca37d95ae48e9;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 84eaaeb2a..82a326c48 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -182,32 +182,35 @@ let is_atomic t = aux_mpres t let add_parens child_prec curr_prec t = -(* eprintf - ("add_parens: " ^^ - "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!") - child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos) - curr_prec; *) - if is_atomic t then t + if is_atomic t then + ((*prerr_endline ("NOT adding parens around ATOMIC: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*)t) else if child_prec >= 0 && child_prec < curr_prec then - begin (* parens should be added *) -(* prerr_endline "adding parens!"; *) + begin + (*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]) end else - t + ((*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 ids_to_uris ?(prec=(-1)) = +let lookup_uri ids_to_uris id = + try + let uri = Hashtbl.find ids_to_uris id in + Some (UriManager.string_of_uri uri) + with Not_found -> None +;; + +let render ~lookup_uri ?(prec=(-1)) = let module A = Ast in let module P = Mpresentation in (* let use_unicode = true in *) - let lookup_uri id = - (try - let uri = Hashtbl.find ids_to_uris id in - Some (UriManager.string_of_uri uri) - with Not_found -> None) - in let make_href xmlattrs xref = let xref_uris = List.fold_right @@ -321,7 +324,6 @@ let render ids_to_uris ?(prec=(-1)) = let expected_level = ref None in let new_xref = ref [] in let new_xmlattrs = ref [] in -(* let reinit = ref false in *) let rec aux_attribute = function | A.AttributedTerm (attr, t) -> @@ -330,7 +332,7 @@ let render ids_to_uris ?(prec=(-1)) = | `Raw _ -> () | `Level (-1) -> reset := true | `Level child_prec -> - assert (!expected_level = None); +(* assert (!expected_level = None); *) expected_level := !inferred_level; inferred_level := Some child_prec | `IdRef xref -> new_xref := xref :: !new_xref @@ -343,14 +345,19 @@ let render ids_to_uris ?(prec=(-1)) = | Some prec -> prec in (match !inferred_level with - | None -> aux !new_xmlattrs mathonly new_xref prec t + | None -> aux !new_xmlattrs mathonly new_xref prec t | Some child_prec -> - let t' = - aux !new_xmlattrs mathonly new_xref child_prec t in + let t' = aux !new_xmlattrs mathonly new_xref child_prec t in + (*prerr_endline + ("inferred: "^string_of_int child_prec^ + " exp: "^string_of_int prec ^ + " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false + (function x::_->x|_->assert false) 80 t');*) if !reset - then t' + then ((*prerr_endline "reset";*)t') else add_parens child_prec prec t') in +(* prerr_endline (CicNotationPp.pp_term t); *) aux_attribute t and aux_literal xmlattrs xref prec l = let attrs = make_href xmlattrs xref in @@ -364,6 +371,9 @@ let render ids_to_uris ?(prec=(-1)) = (* use the one below to reset precedence and associativity *) let invoke_reinit t = aux [] mathonly xref ~-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) @@ -374,6 +384,16 @@ let render ids_to_uris ?(prec=(-1)) = | 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) @@ -383,6 +403,20 @@ let render ids_to_uris ?(prec=(-1)) = (CicNotationUtil.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 + (CicNotationUtil.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 + (CicNotationUtil.ungroup terms))) + | A.Maction alternatives -> + toggle_action (List.map invoke_reinit alternatives) | A.Group terms -> let children = aux_children mathonly false xref prec