From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 11:22:13 +0000 (+0000)
Subject: added metas local context maction: ?n[...]
X-Git-Tag: make_still_working~6839
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92029d709642b641888f6383c169c9f2ece4ebf7;p=helm.git

added metas local context maction: ?n[...]
---

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 297a52bc5..4198e83b0 100644
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/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/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 4c8bbc7d4..96a15c01e 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/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 _