From 3208e22ea89c459a5a7944ad8e82511d4a5328fa Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 16 Aug 2016 16:17:20 +0200
Subject: Added raw printing of types without formatting.

This avoids introducing line breaks during printing of function
types.
Bug 18004
---
 cparser/Cprint.ml  | 11 ++++++++---
 cparser/Cprint.mli |  1 +
 cparser/Elab.ml    |  4 ++--
 3 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index e80a4c8e..2a110104 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -126,7 +126,7 @@ let name_of_fkind = function
   | FDouble -> "double"
   | FLongDouble -> "long double"
 
-let rec dcl pp ty n =
+let rec dcl ?(pp_indication=true) pp ty n =
   match ty with
   | TVoid a ->
       fprintf pp "void%a%t" attributes a n
@@ -160,7 +160,8 @@ let rec dcl pp ty n =
         | [] -> n pp
         | _  -> fprintf pp " (%a%t)" attributes a n
         end;
-        fprintf pp "(@[<hov 0>";
+        fprintf pp "(";
+        if pp_indication then fprintf pp "@[<hov 0>";
         begin match args with
         | None -> ()
         | Some [] -> if vararg then fprintf pp "..." else fprintf pp "void"
@@ -169,7 +170,8 @@ let rec dcl pp ty n =
             List.iter (fun a -> fprintf pp ",@ "; param a) al;
             if vararg then fprintf pp ",@ ..."
         end;
-        fprintf pp "@])" in
+        if pp_indication then fprintf pp "@]";
+        fprintf pp ")" in
       dcl pp tres n'
   | TNamed(id, a) ->
       fprintf pp "%a%a%t" ident id attributes a n
@@ -183,6 +185,9 @@ let rec dcl pp ty n =
 let typ pp ty =
   dcl pp ty (fun _ -> ())
 
+let typ_raw pp ty =
+  dcl ~pp_indication:false pp ty (fun _ -> ())
+
 type associativity = LtoR | RtoL | NA
 
 let precedence = function               (* H&S section 7.2 *)
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index 349b5f9a..fe71e4fe 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -20,6 +20,7 @@ val print_debug_idents : bool ref
 val location : Format.formatter -> C.location -> unit
 val attributes : Format.formatter -> C.attributes -> unit
 val typ : Format.formatter -> C.typ -> unit
+val typ_raw : Format.formatter -> C.typ -> unit
 val simple_decl : Format.formatter -> C.ident * C.typ -> unit
 val full_decl: Format.formatter -> C.decl -> unit
 val const : Format.formatter -> C.constant -> unit
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index e3a0ef0c..52426014 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -42,8 +42,8 @@ let warning loc =
 let print_typ env fmt ty =
   match ty with
   | TNamed _  ->
-      Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ ty Cprint.typ (Cutil.unroll env ty)
-  | _ -> Format.fprintf fmt "'%a'" Cprint.typ ty
+      Format.fprintf fmt "'%a' (aka '%a')" Cprint.typ_raw ty Cprint.typ_raw (Cutil.unroll env ty)
+  | _ -> Format.fprintf fmt "'%a'" Cprint.typ_raw ty
 
 (* Error reporting for Env functions *)
 
-- 
cgit