From 04e22abe4378e29671def7b4d9c7e509c58ef6b6 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 31 Mar 2020 19:12:18 +0200
Subject: [primitive floats] Add low level hexadecimal printing

---
 interp/constrextern.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3f7bb6e330..bb91dc28da 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -888,12 +888,19 @@ let q_infinity () = qualid_of_ref "num.float.infinity"
 let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
 let q_nan () = qualid_of_ref "num.float.nan"
 
+let get_printing_float = Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Float"]
+    ~value:true
+
 let extern_float f scopes =
   if Float64.is_nan f then CRef(q_nan (), None)
   else if Float64.is_infinity f then CRef(q_infinity (), None)
   else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
   else
-    let s = Float64.(to_string f) in
+    let s =
+      let hex = !Flags.raw_print || not (get_printing_float ()) in
+      if hex then Float64.to_hex_string f else Float64.to_string f in
     let n = NumTok.Signed.of_string s in
     extern_prim_token_delimiter_if_required (Numeral n)
       "float" "float_scope" scopes
-- 
cgit v1.2.3