diff options
Diffstat (limited to 'lib/pp.ml4')
| -rw-r--r-- | lib/pp.ml4 | 45 |
1 files changed, 27 insertions, 18 deletions
@@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp_control (* This should not be used outside of this file. Use @@ -160,6 +158,17 @@ let tclose () = [< 'Ppcmd_close_tbox >] let (++) = Stream.iapp +let rec eval_ppcmds l = + let rec aux l = + try + let a = match Stream.next l with + | Ppcmd_box (b,s) -> Ppcmd_box (b,eval_ppcmds s) + | a -> a in + let rest = aux l in + a :: rest + with Stream.Failure -> [] in + Stream.of_list (aux l) + (* In new syntax only double quote char is escaped by repeating it *) let rec escape_string s = let rec escape_at s i = @@ -270,28 +279,21 @@ let pp_dirs ft = try Stream.iter pp_dir dirstream; com_brk ft with - | e -> Format.pp_print_flush ft () ; raise e + | reraise -> Format.pp_print_flush ft () ; raise reraise (* pretty print on stdout and stderr *) -let pp_std_dirs = pp_dirs !std_ft -let pp_err_dirs = pp_dirs !err_ft - -let ppcmds x = Ppdir_ppcmds x - (* Special chars for emacs, to detect warnings inside goal output *) -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 mt() else str emacs_warning_start_string +let emacs_quote_start = String.make 1 (Char.chr 254) +let emacs_quote_end = String.make 1 (Char.chr 255) -let warnend() = - if not !print_emacs then mt() else str emacs_warning_end_string +let emacs_quote strm = + if !print_emacs then + [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >] + else hov 0 strm -let warnbody strm = - [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >] +let warnbody strm = emacs_quote (str "Warning: " ++ strm) (* pretty printing functions WITHOUT FLUSH *) let pp_with ft strm = @@ -339,3 +341,10 @@ let msgnl x = msgnl_with !std_ft x let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x + +(* Same specific display in emacs as warning, but without the "Warning:" *) +let msg_debug x = msgnl (emacs_quote x) + +let string_of_ppcmds c = + msg_with Format.str_formatter c; + Format.flush_str_formatter () |