]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPres.ml
snapshot
[helm.git] / helm / ocaml / cic_notation / cicNotationPres.ml
index 83bb10878518d0e0eb7eeda8fb1e410e5516e722..c3ea73f1c95491aec319a37aa880a8665ba53085 100644 (file)
@@ -31,6 +31,7 @@ type markup = mathml_markup
 let atop_attributes = [None, "linethickness", "0pt"]
 let binder_attributes = [None, "mathcolor", "blue"]
 let indent_attributes = [None, "indent", "1em"]
+let keyword_attributes = [None, "mathcolor", "blue"]
 
 let mpres_arrow = Mpresentation.Mo (binder_attributes, "->")
   (* TODO unicode symbol "to" *)
@@ -214,8 +215,8 @@ let render ids_to_uris =
   and aux_literal xref prec uris l =
     let attrs = make_href xref uris in
       match l with
-       | `Symbol s
-       | `Keyword s -> P.Mo (attrs, to_unicode s)
+       | `Symbol s -> P.Mo (attrs, to_unicode s)
+       | `Keyword s -> P.Mo (keyword_attributes @ attrs, to_unicode s)
        | `Number s  -> P.Mn (attrs, to_unicode s)
   and aux_layout mathonly xref pos prec uris l =
     let attrs = make_xref xref in