initial support for notation that specifies the precedence of term variables, that...

[helm.git] / helm / software / components / content_pres / cicNotationPres.ml

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 297a52bc5d7c09050af98740aba7cb0a51ae94ce..a7bce6437520b8c36361deac9e29e6fe225cf5e8 100644 (file)
--- 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 ([], ";")
@@ -194,7 +197,7 @@ let add_parens child_prec child_assoc child_pos curr_prec t =
           child_assoc = Gramext.RightA &&
           child_pos <> `Right))
   then begin (* parens should be added *)
-(*     prerr_endline "adding parens!"; *)
+(*      prerr_endline "adding parens!";  *)
     match t with
     | Mpresentation.Mobject (_, box) ->
         mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
@@ -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
@@ -306,7 +324,8 @@ let render ids_to_uris ?(prec=(-1)) =
         assert false
   and aux_attributes xmlattrs mathonly xref pos 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
@@ -319,14 +338,21 @@ let render ids_to_uris ?(prec=(-1)) =
           | `Raw _ -> ()
           | `Level (-1, _) -> reset := true
           | `Level (child_prec, child_assoc) ->
-              new_level := Some (child_prec, child_assoc)
+              assert (!expected_level = None);
+              expected_level := !inferred_level;
+              inferred_level := Some (child_prec, child_assoc)
           | `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
+          let prec = 
+            match !expected_level with
+            | None -> prec
+            | Some (prec, _) -> prec
+          in
+          (match !inferred_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
@@ -339,7 +365,7 @@ let render ids_to_uris ?(prec=(-1)) =
     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