From 12ff38155f52e02b7e605a6970b997bc30eacb87 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 11:22:13 +0000 Subject: [PATCH] added metas local context maction: ?n[...] --- components/content_pres/cicNotationPres.ml | 18 ++++++++++++++++++ components/content_pres/termContentPres.ml | 7 ++----- 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/components/content_pres/cicNotationPres.ml b/components/content_pres/cicNotationPres.ml index 297a52bc5..4198e83b0 100644 --- a/components/content_pres/cicNotationPres.ml +++ b/components/content_pres/cicNotationPres.ml @@ -135,9 +135,12 @@ let box_of mathonly spec attrs 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 ([], ";") @@ -296,6 +299,21 @@ let render ids_to_uris ?(prec=(-1)) = 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 pos 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 diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index 4c8bbc7d4..96a15c01e 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -232,12 +232,9 @@ let pp_ast0 t k = | Ast.Implicit -> builtin_symbol "?" | Ast.Meta (n, l) -> let local_context l = - CicNotationUtil.dress (builtin_symbol ";") - (List.map (function None -> builtin_symbol "_" | Some t -> k t) l) + List.map (function None -> None | Some t -> Some (k t)) l in - hbox false false - ([ builtin_symbol "?"; number (string_of_int n) ] - @ (if l <> [] then local_context l else [])) + Ast.Meta(n, local_context l) | Ast.Sort sort -> aux_sort sort | Ast.Num _ | Ast.Symbol _ -- 2.39.2