4 files changed, 42 insertions, 27 deletions
diff --git a/lib/options.ml b/lib/options.ml
index e59a19bbb..848b08611 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -63,6 +63,10 @@ let if_verbose f x = if not !silent then f x
 
 let hash_cons_proofs = ref true
 
+let warn = ref true
+let make_warn flag = warn := flag;  ()
+let if_warn f x = if !warn then f x
+
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
diff --git a/lib/options.mli b/lib/options.mli
index 7fa55e636..73962735d 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -40,6 +40,9 @@ val silently : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
+val make_warn : bool -> unit
+val if_warn : ('a -> unit) -> 'a -> unit
+
 val hash_cons_proofs : bool ref
 
 (* Temporary activate an option ('c must be an atomic type) *)
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 27ddae00c..bfabb533b 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -130,19 +130,15 @@ let align () = [< 'Ppcmd_print_break (0,0) >]
 let int n = str (string_of_int n)
 let real r = str (string_of_float r)
 let bool b = str (string_of_bool b)
-
-(* In new syntax only double quote char is escaped by repeating it *)
-let rec escape_string s =
-  let rec escape_at s i =
-    if i<0 then s
-    else if s.[i] == '"' then
-      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
-      escape_at s' (i-1)
-    else escape_at s (i-1) in
-  escape_at s (String.length s - 1)
-
-let qstring s = str ("\""^escape_string s^"\"")
-let qs = qstring
+let strbrk s =
+  let rec aux p n =
+    if n < String.length s then 
+      if s.[n] = ' ' then
+	if p=n then [< spc (); aux (n+1) (n+1) >]
+	else [< str (String.sub s p (n-p)); spc (); aux (n+1) (n+1) >]
+      else aux p (n+1)
+    else if p=n then [< >] else [< str (String.sub s p (n-p)) >]
+  in aux 0 0
 
 (* boxing commands *)
 let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
@@ -162,6 +158,20 @@ let tclose () = [< 'Ppcmd_close_tbox >]
 
 let (++) = Stream.iapp
 
+(* In new syntax only double quote char is escaped by repeating it *)
+let rec escape_string s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '"' then
+      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstring s = str ("\""^escape_string s^"\"")
+let qs = qstring
+let quote s = h 0 (str "\"" ++ s ++ str "\"")
+
 (* This flag tells if the last printed comment ends with a newline, to
   avoid empty lines *)
 let com_eol = ref false
@@ -252,11 +262,13 @@ let emacs_warning_start_string = String.make 1 (Char.chr 254)
 let emacs_warning_end_string = String.make 1 (Char.chr 255)
 
 let warnstart() = 
-  if not !print_emacs then str "" else str emacs_warning_start_string
+  if not !print_emacs then mt() else str emacs_warning_start_string
 
 let warnend() = 
-  if not !print_emacs then str "" else str emacs_warning_end_string
-  
+  if not !print_emacs then mt() else str emacs_warning_end_string
+
+let warnbody strm =
+  [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
@@ -265,21 +277,17 @@ let pp_with ft strm =
 let ppnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
 
-
-let default_warn_with ft pps = 
-  ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >]
+let default_warn_with ft strm = ppnl_with ft (warnbody strm)
 
 let pp_warn_with = ref default_warn_with
 
 let set_warning_function pp_warn = pp_warn_with := pp_warn
 
-let warn_with ft pps = !pp_warn_with ft pps 
+let warn_with ft strm = !pp_warn_with ft strm
 
 let warning_with ft string = warn_with ft (str string)
 
-let pp_flush_with ft =
-  Format.pp_print_flush ft
-
+let pp_flush_with ft = Format.pp_print_flush ft
 
 (* pretty printing functions WITH FLUSH *)
 let msg_with ft strm =
@@ -288,10 +296,8 @@ let msg_with ft strm =
 let msgnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
 
-let msg_warning_with ft strm=
-  pp_dirs ft [< 'Ppdir_ppcmds [< warnstart() ; str "Warning: "; strm ; warnend() >]; 
-		'Ppdir_print_newline >]
-
+let msg_warning_with ft strm =
+  msgnl_with ft (warnbody strm)
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp        x = pp_with   !std_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
index a0177d741..8a5aee799 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -53,6 +53,8 @@ val real : float -> std_ppcmds
 val bool : bool -> std_ppcmds
 val qstring : string -> std_ppcmds
 val qs : string -> std_ppcmds
+val quote : std_ppcmds -> std_ppcmds
+val strbrk : string -> std_ppcmds
 
 (*s Boxing commands. *)