X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FcicNotationPres.ml;h=673df335f224d4db81427637f1c185bb31e2a9bb;hb=refs%2Ftags%2F0.4.95;hp=308f23d22a13ea4826cde1050c8fbdc24a672c04;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/content_pres/cicNotationPres.ml b/components/content_pres/cicNotationPres.ml
index 308f23d22..673df335f 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 ([], ";")
@@ -202,7 +205,7 @@ let add_parens child_prec child_assoc child_pos curr_prec t =
   end else
     t
 
-let render ids_to_uris =
+let render ids_to_uris ?(prec=(-1)) =
   let module A = Ast in
   let module P = Mpresentation in
 (*   let use_unicode = true in *)
@@ -296,6 +299,21 @@ let render ids_to_uris =
             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
@@ -339,7 +357,7 @@ let render ids_to_uris =
     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 =
     let attrs = make_xref xref in
@@ -418,7 +436,7 @@ let render ids_to_uris =
     in
       List.map boxify_pres (find_clusters terms)
   in
-  aux [] false (ref []) `Inner ~-1
+  aux [] false (ref []) `Inner prec
 
 let rec print_box (t: boxml_markup) =
   Box.box2xml print_mpres t