added XmlAttrs attribute for specification of xml attributes directly

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 207b26a233d139773815234a62843838e115020d..e72bfacc8fc8f31da17982b27a0bda3be1b8f78e 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -37,8 +37,6 @@ type term_info =
     uri: (Cic.id, string) Hashtbl.t;
   }
 
-let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
-
 let get_types uri =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
@@ -81,9 +79,17 @@ let resolve_binder = function
   | `Forall -> "\\forall"
   | `Exists -> "\\exists"
 
+let binder_attributes = [None, "mathcolor", "blue"]
+let atop_attributes = [None, "linethickness", "0pt"]
+let indent_attributes = [None, "indent", "1em"]
+let keyword_attributes = [None, "mathcolor", "blue"]
+
 let pp_ast0 t k =
   let reset_href t = Ast.AttributedTerm (`Href [], t) in
   let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in
+  let binder_symbol s =
+    Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s)
+  in
   let rec aux = function
     | Ast.Appl ts ->
         Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
@@ -94,13 +100,13 @@ let pp_ast0 t k =
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             aux_ty ty;
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              builtin_symbol "\\to";
+              binder_symbol "\\to";
               k body]))])))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              builtin_symbol (resolve_binder binder_kind);
+              binder_symbol (resolve_binder binder_kind);
               k id;
               builtin_symbol ":";
               aux_ty ty ]));
@@ -275,6 +281,8 @@ let instantiate21 env (* precedence associativity *) l1 =
         assert (CicNotationEnv.well_typed expected_ty value);
         [ CicNotationEnv.term_of_value value ]
     | Ast.Magic m -> subst_magic env m
+    | Ast.Literal (`Keyword k) as t ->
+        [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ]
     | Ast.Literal _ as t -> [ t ]
     | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
     | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]