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 ([], ";")
in
aux_mpres t
-let add_parens child_prec child_assoc child_pos 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
- else if child_prec >= 0
- && (child_prec < curr_prec
- || (child_prec = curr_prec &&
- child_assoc = Gramext.LeftA &&
- child_pos <> `Left)
- || (child_prec = curr_prec &&
- child_assoc = Gramext.RightA &&
- child_pos <> `Right))
- then begin (* parens should be added *)
-(* prerr_endline "adding parens!"; *)
+let add_parens child_prec curr_prec 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
+ (*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
in
(* when mathonly is true no boxes should be generated, only mrows *)
(* "xref" is *)
- let rec aux xmlattrs mathonly xref pos prec t =
+ let rec aux xmlattrs mathonly xref prec t =
match t with
| A.AttributedTerm _ ->
- aux_attributes xmlattrs mathonly xref pos prec t
+ aux_attributes xmlattrs mathonly xref prec t
| A.Num (literal, _) ->
let attrs =
(RenderingAttrs.number_attributes `MathML)
box_of mathonly (A.H, false, false) [] [
Mpres.Mi ([], name);
Mpres.Mo ([], to_unicode "\\def");
- aux [] mathonly xref pos prec t ])
+ 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 ])
+ | A.Meta(n, l) ->
+ let local_context l =
+ box_of mathonly (A.H, false, false) []
+ ([ Mpres.Mtext ([], "[") ] @
+ (CicNotationUtil.dress (Mpres.Mtext ([], ";"))
+ (List.map
+ (function
+ | None -> Mpres.Mtext ([], "_")
+ | Some t -> aux xmlattrs mathonly xref prec t) l)) @
+ [ Mpres.Mtext ([], "]")])
+ 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 pos prec l
+ | A.Layout l -> aux_layout mathonly xref prec l
| A.Magic _
| A.Variable _ -> assert false (* should have been instantiated *)
| t ->
prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t);
assert false
- and aux_attributes xmlattrs mathonly xref pos prec t =
+ and aux_attributes xmlattrs mathonly xref prec t =
let reset = ref false in
- let new_level = ref None in
+ let inferred_level = ref None in
+ let expected_level = ref None in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
- let new_pos = ref pos in
-(* let reinit = ref false in *)
let rec aux_attribute =
function
| A.AttributedTerm (attr, t) ->
(match attr with
| `Loc _
| `Raw _ -> ()
- | `Level (-1, _) -> reset := true
- | `Level (child_prec, child_assoc) ->
- new_level := Some (child_prec, child_assoc)
+ | `Level (-1) -> reset := true
+ | `Level child_prec ->
+(* assert (!expected_level = None); *)
+ expected_level := !inferred_level;
+ inferred_level := Some child_prec
| `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 !new_pos prec t
- | Some (child_prec, child_assoc) ->
- let t' =
- aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in
+ let prec =
+ match !expected_level with
+ | None -> prec
+ | Some prec -> prec
+ in
+ (match !inferred_level with
+ | None -> aux !new_xmlattrs mathonly new_xref prec t
+ | Some child_prec ->
+ 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'
- else add_parens child_prec child_assoc !new_pos prec 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
(match l with
| `Symbol s -> Mpres.Mo (attrs, to_unicode s)
- | `Keyword 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 pos prec l =
+ and aux_layout mathonly xref prec l =
let attrs = make_xref xref in
- let invoke' t = aux [] true (ref []) pos prec t in
+ let invoke' t = aux [] true (ref []) prec t in
(* use the one below to reset precedence and associativity *)
- let invoke_reinit t = aux [] mathonly xref `Inner ~-1 t in
+ 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)
| 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) ->
let children =
- aux_children mathonly spacing xref pos prec
+ aux_children mathonly spacing xref prec
(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 pos prec
+ aux_children mathonly false xref prec
(CicNotationUtil.ungroup terms)
in
box_of mathonly (A.H, false, false) attrs children
| A.Break -> assert false (* TODO? *)
- and aux_children mathonly spacing xref pos prec terms =
+ and aux_children mathonly spacing xref prec terms =
let find_clusters =
let rec aux_list first clusters acc =
function
| (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 hd :: acc) []
+ (aux [] mathonly xref 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 *)
aux_list false clusters
- (aux [] mathonly xref pos prec hd :: acc) tl
+ (aux [] mathonly xref prec hd :: acc) tl
in
aux_list true [] []
in
in
List.map boxify_pres (find_clusters terms)
in
- aux [] false (ref []) `Inner prec
+ aux [] false (ref []) prec
let rec print_box (t: boxml_markup) =
Box.box2xml print_mpres t
projects / helm.git / blobdiff