diff options
| author | Emilio Jesus Gallego Arias | 2016-12-05 18:17:46 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:38 +0100 |
| commit | a8ec2dc5c330ded1ba400ef202c57e68d2533312 (patch) | |
| tree | f333e6c9367c51f7a3c208413d3fb607916a724e /toplevel | |
| parent | 6885a398229918865378ea24f07d93d2bcdd2802 (diff) | |
[pp] Remove special tag type and handler from Pp.
For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.
We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.
This is a step towards moving the last bit of terminal code out of the
core system.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
3 files changed, 4 insertions, 9 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e9506803df..43807c1ca6 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -14,7 +14,7 @@ open Vernac open Pcoq let top_stderr x = - Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 823d05580b..268d40c91d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -311,18 +311,13 @@ let print_style_tags () = let tags = Ppstyle.dump () in let iter (t, st) = let st = match st with Some st -> st | None -> Terminal.make () in - let opt = - Terminal.eval st ^ - String.concat "." (Ppstyle.repr t) ^ - Terminal.reset ^ "\n" - in + let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in print_string opt in let make (t, st) = match st with | None -> None | Some st -> let tags = List.map string_of_int (Terminal.repr st) in - let t = String.concat "." (Ppstyle.repr t) in Some (t ^ "=" ^ String.concat ";" tags) in let repr = List.map_filter make tags in @@ -445,7 +440,7 @@ let get_native_name s = with the appropriate error code *) let fatal_error info anomaly = let msg = info ++ fnl () in - Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ?pp_tag:None) msg; + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; exit (if anomaly then 129 else 1) let parse_args arglist = diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 4fc4540c1c..06908abb6e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -181,7 +181,7 @@ let pp_cmd_header loc com = *) (* FIXME *) let print_cmd_header loc com = - Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com); + Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Topfmt.std_ft () let rec interp_vernac po chan_beautify checknav (loc,com) = |