aboutsummaryrefslogtreecommitdiffstats
path: root/lib
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-01-25 20:11:09 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-01-25 20:11:09 +0100
commit35c7398e985c51a765c6bbf08719d9df7c285f9c (patch)
treebf49c213bb115c9db418eabe66e11affa9f1db82 /lib
parent4467453e0edca993c175690b7141d4916af3dc19 (diff)
downloadcompcert-35c7398e985c51a765c6bbf08719d9df7c285f9c.tar.gz
compcert-35c7398e985c51a765c6bbf08719d9df7c285f9c.zip
Added printer for Configuration and finished Clflags.
Diffstat (limited to 'lib')
-rw-r--r--lib/Json.ml9
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/Json.ml b/lib/Json.ml
index db2de5d4..4aa91e95 100644
--- a/lib/Json.ml
+++ b/lib/Json.ml
@@ -31,3 +31,12 @@ let p_jbool oc = fprintf oc "%B"
(* Print a int as json int *)
let p_jint oc = fprintf oc "%d"
+
+(* Print a member *)
+let p_jmember oc name p_mem mem =
+ fprintf oc "\n%a:%a" p_jstring name p_mem mem
+
+(* Print optional value *)
+let p_jopt p_elem oc = function
+ | None -> output_string oc "null"
+ | Some i -> p_elem oc i