added find&replace facility

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

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index 790bb3785088a8b67c7dc905fcefa66919d8b4bd..c3ea73f1c95491aec319a37aa880a8665ba53085 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -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" *)
@@ -142,8 +143,8 @@ let is_atomic t =
   aux_mpres t
 
 let add_parens child_prec child_assoc child_pos curr_prec t =
-  prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec
-    (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec));
+(*  prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec
+    (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec)); *)
   if is_atomic t then t
   else if child_prec < curr_prec
     || (child_prec = curr_prec &&
@@ -211,12 +212,11 @@ let render ids_to_uris =
         add_parens child_prec child_assoc pos prec t'
     | `IdRef xref -> aux mathonly (Some xref) pos prec uris t
     | `Href uris' -> aux mathonly xref pos prec uris' t
-    | _ -> assert false
   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