aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-14 16:40:28 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-20 15:20:32 +0200
commitf4584f8a332c9077844e227c8b86d3cb1daf8b12 (patch)
tree8f09f14d3a3273ccdbd7ec86146b70bce5623278 /ide/coqOps.ml
parent481d2b681463d2758fec6b2417631491be69f216 (diff)
Adding rich printing primitives.
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index e97a2ecee..6a7c2e819 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -164,6 +164,14 @@ let flags_to_color f =
else if List.mem `INCOMPLETE f then `NAME "gray"
else `NAME Preferences.processed_color#get
+let validate s =
+ let open Xml_datatype in
+ let rec validate = function
+ | PCData s -> Glib.Utf8.validate s
+ | Element (_, _, children) -> List.for_all validate children
+ in
+ validate (Richpp.repr s)
+
module Doc = Document
class coqops