From 14155762a7cd46ed6a3e9cf2a58e11ee1244b188 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 18:31:05 +0200 Subject: [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list` This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags. --- lib/pp.ml | 24 +++--------------------- 1 file changed, 3 insertions(+), 21 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index a51b4458fb..57d630a69c 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -42,25 +42,7 @@ end = struct end -module Tag : -sig - type t - type 'a key - val create : string -> 'a key - val inj : 'a -> 'a key -> t - val prj : t -> 'a key -> 'a option -end = -struct - -module Dyn = Dyn.Make(struct end) - -type t = Dyn.t -type 'a key = 'a Dyn.tag -let create = Dyn.create -let inj = Dyn.Easy.inj -let prj = Dyn.Easy.prj - -end +type pp_tag = string list open Pp_control @@ -95,7 +77,7 @@ type 'a ppcmd_token = | Ppcmd_open_box of block_type | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_open_tag of Tag.t + | Ppcmd_open_tag of pp_tag | Ppcmd_close_tag type 'a ppdir_token = @@ -243,7 +225,7 @@ let rec pr_com ft s = Some s2 -> Format.pp_force_newline ft (); pr_com ft s2 | None -> () -type tag_handler = Tag.t -> Format.tag +type tag_handler = pp_tag -> Format.tag (* pretty printing functions *) let pp_dirs ?pp_tag ft = -- cgit v1.2.3 From 2617a83e572531e26734cff8b9eb8aa09d49b850 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Sep 2016 16:33:47 +0200 Subject: [pp] Remove `Pp.stras`. Mostly unused, we ought to limit spacing in the boxes themselves. --- lib/pp.ml | 34 ++++++++++++---------------------- 1 file changed, 12 insertions(+), 22 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 57d630a69c..9d2445d490 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -58,18 +58,14 @@ open Pp_control *) type block_type = - | Pp_hbox of int - | Pp_vbox of int - | Pp_hvbox of int + | Pp_hbox of int + | Pp_vbox of int + | Pp_hvbox of int | Pp_hovbox of int -type str_token = -| Str_def of string -| Str_len of string * int (** provided length *) - -type 'a ppcmd_token = - | Ppcmd_print of 'a - | Ppcmd_box of block_type * ('a ppcmd_token Glue.t) +type ppcmd_token = + | Ppcmd_string of string + | Ppcmd_box of block_type * (ppcmd_token Glue.t) | Ppcmd_print_break of int * int | Ppcmd_white_space of int | Ppcmd_force_newline @@ -81,11 +77,11 @@ type 'a ppcmd_token = | Ppcmd_close_tag type 'a ppdir_token = - | Ppdir_ppcmds of 'a ppcmd_token Glue.t + | Ppdir_ppcmds of ppcmd_token Glue.t | Ppdir_print_newline | Ppdir_print_flush -type ppcmd = str_token ppcmd_token +type ppcmd = ppcmd_token type std_ppcmds = ppcmd Glue.t @@ -134,8 +130,7 @@ let utf8_length s = !cnt (* formatting commands *) -let str s = Glue.atom(Ppcmd_print (Str_def s)) -let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i))) +let str s = Glue.atom(Ppcmd_string s) let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b)) let fnl () = Glue.atom(Ppcmd_force_newline) let pifb () = Glue.atom(Ppcmd_print_if_broken) @@ -236,14 +231,9 @@ let pp_dirs ?pp_tag ft = | Pp_hovbox n -> Format.pp_open_hovbox ft n in let rec pp_cmd = function - | Ppcmd_print tok -> - begin match tok with - | Str_def s -> - let n = utf8_length s in - Format.pp_print_as ft n s - | Str_len (s, n) -> - Format.pp_print_as ft n s - end + | Ppcmd_string str -> + let n = utf8_length str in + Format.pp_print_as ft n str | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) pp_open_box bty ; if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss; -- cgit v1.2.3 From 8f8af9e4ebf1ea1ed15f765196ef5af8a77d3c27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:06:43 +0200 Subject: [pp] Prepare for serialization, remove opaque glue. We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter. --- lib/pp.ml | 184 +++++++++++++++++++++----------------------------------------- 1 file changed, 62 insertions(+), 122 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 9d2445d490..6d7bdf75e3 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -6,44 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module Glue : sig - - (** The [Glue] module implements a container data structure with - efficient concatenation. *) - - type 'a t - - val atom : 'a -> 'a t - val glue : 'a t -> 'a t -> 'a t - val empty : 'a t - val is_empty : 'a t -> bool - val iter : ('a -> unit) -> 'a t -> unit - -end = struct - - type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t - - let atom x = GLeaf x - - let glue x y = - match x, y with - | GEmpty, _ -> y - | _, GEmpty -> x - | _, _ -> GNode (x,y) - - let empty = GEmpty - - let is_empty x = x = GEmpty - - let rec iter f = function - | GEmpty -> () - | GLeaf x -> f x - | GNode (x,y) -> iter f x; iter f y - -end - -type pp_tag = string list - open Pp_control (* The different kinds of blocks are: @@ -63,36 +25,22 @@ type block_type = | Pp_hvbox of int | Pp_hovbox of int -type ppcmd_token = +type pp_tag = string list + +type std_ppcmds = + | Ppcmd_empty | Ppcmd_string of string - | Ppcmd_box of block_type * (ppcmd_token Glue.t) + | Ppcmd_glue of std_ppcmds * std_ppcmds + | Ppcmd_box of block_type * std_ppcmds | Ppcmd_print_break of int * int | Ppcmd_white_space of int | Ppcmd_force_newline - | Ppcmd_print_if_broken | Ppcmd_open_box of block_type | Ppcmd_close_box | Ppcmd_comment of string list | Ppcmd_open_tag of pp_tag | Ppcmd_close_tag -type 'a ppdir_token = - | Ppdir_ppcmds of ppcmd_token Glue.t - | Ppdir_print_newline - | Ppdir_print_flush - -type ppcmd = ppcmd_token - -type std_ppcmds = ppcmd Glue.t - -type 'a ppdirs = 'a ppdir_token Glue.t - -let (++) = Glue.glue - -let app = Glue.glue - -let is_empty g = Glue.is_empty g - (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) Rem 2 : if used for an iso8859_1 encoded string, the result is @@ -129,22 +77,30 @@ let utf8_length s = done ; !cnt +let app s1 s2 = match s1, s2 with + | Ppcmd_empty, s + | s, Ppcmd_empty -> s + | s1, s2 -> Ppcmd_glue(s1, s2) + +let (++) = app + (* formatting commands *) -let str s = Glue.atom(Ppcmd_string s) -let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b)) -let fnl () = Glue.atom(Ppcmd_force_newline) -let pifb () = Glue.atom(Ppcmd_print_if_broken) -let ws n = Glue.atom(Ppcmd_white_space n) -let comment l = Glue.atom(Ppcmd_comment l) +let str s = Ppcmd_string s +let brk (a,b) = Ppcmd_print_break (a,b) +let fnl () = Ppcmd_force_newline +let ws n = Ppcmd_white_space n +let comment l = Ppcmd_comment l (* derived commands *) -let mt () = Glue.empty -let spc () = Glue.atom(Ppcmd_print_break (1,0)) -let cut () = Glue.atom(Ppcmd_print_break (0,0)) -let align () = Glue.atom(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) +let mt () = Ppcmd_empty +let spc () = Ppcmd_print_break (1,0) +let cut () = Ppcmd_print_break (0,0) +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) + +(* XXX: To Remove *) let strbrk s = let rec aux p n = if n < String.length s then @@ -153,7 +109,7 @@ let strbrk s = 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 List.fold_left (++) Glue.empty (aux 0 0) + in List.fold_left (++) Ppcmd_empty (aux 0 0) let pr_loc_pos loc = if Loc.is_ghost loc then (str"") @@ -174,26 +130,25 @@ let pr_loc loc = int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ str":" ++ fnl()) -let ismt = is_empty +let ismt = function | Ppcmd_empty -> true | _ -> false (* boxing commands *) -let h n s = Glue.atom(Ppcmd_box(Pp_hbox n,s)) -let v n s = Glue.atom(Ppcmd_box(Pp_vbox n,s)) -let hv n s = Glue.atom(Ppcmd_box(Pp_hvbox n,s)) -let hov n s = Glue.atom(Ppcmd_box(Pp_hovbox n,s)) +let h n s = Ppcmd_box(Pp_hbox n,s) +let v n s = Ppcmd_box(Pp_vbox n,s) +let hv n s = Ppcmd_box(Pp_hvbox n,s) +let hov n s = Ppcmd_box(Pp_hovbox n,s) (* Opening and closing of boxes *) -let hb n = Glue.atom(Ppcmd_open_box(Pp_hbox n)) -let vb n = Glue.atom(Ppcmd_open_box(Pp_vbox n)) -let hvb n = Glue.atom(Ppcmd_open_box(Pp_hvbox n)) -let hovb n = Glue.atom(Ppcmd_open_box(Pp_hovbox n)) -let close () = Glue.atom(Ppcmd_close_box) +let hb n = Ppcmd_open_box(Pp_hbox n) +let vb n = Ppcmd_open_box(Pp_vbox n) +let hvb n = Ppcmd_open_box(Pp_hvbox n) +let hovb n = Ppcmd_open_box(Pp_hovbox n) +let close () = Ppcmd_close_box (* Opening and closed of tags *) -let open_tag t = Glue.atom(Ppcmd_open_tag t) -let close_tag () = Glue.atom(Ppcmd_close_tag) +let open_tag t = Ppcmd_open_tag t +let close_tag () = Ppcmd_close_tag let tag t s = open_tag t ++ s ++ close_tag () -let eval_ppcmds l = l (* In new syntax only double quote char is escaped by repeating it *) let escape_string s = @@ -223,27 +178,27 @@ let rec pr_com ft s = type tag_handler = pp_tag -> Format.tag (* pretty printing functions *) -let pp_dirs ?pp_tag ft = - let pp_open_box = function +let pp_with ?pp_tag ft = + let cpp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n | Pp_hvbox n -> Format.pp_open_hvbox ft n | Pp_hovbox n -> Format.pp_open_hovbox ft n in - let rec pp_cmd = function - | Ppcmd_string str -> - let n = utf8_length str in - Format.pp_print_as ft n str + let rec pp_cmd = let open Format in function + | Ppcmd_empty -> () + | Ppcmd_glue(s1,s2) -> pp_cmd s1; pp_cmd s2 + | Ppcmd_string str -> let n = utf8_length str in + pp_print_as ft n str | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - pp_open_box bty ; - if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss; + cpp_open_box bty ; + if not (Format.over_max_boxes ()) then pp_cmd ss; Format.pp_close_box ft () - | Ppcmd_open_box bty -> pp_open_box bty - | Ppcmd_close_box -> Format.pp_close_box ft () - | Ppcmd_white_space n -> Format.pp_print_break ft n 0 - | Ppcmd_print_break(m,n) -> Format.pp_print_break ft m n - | Ppcmd_force_newline -> Format.pp_force_newline ft () - | Ppcmd_print_if_broken -> Format.pp_print_if_newline ft () + | Ppcmd_open_box bty -> cpp_open_box bty + | Ppcmd_close_box -> pp_close_box ft () + | Ppcmd_white_space n -> pp_print_break ft n 0 + | Ppcmd_print_break(m,n) -> pp_print_break ft m n + | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms | Ppcmd_open_tag tag -> begin match pp_tag with @@ -256,34 +211,19 @@ let pp_dirs ?pp_tag ft = | Some _ -> Format.pp_close_tag ft () end in - let pp_dir = function - | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream - | Ppdir_print_newline -> Format.pp_print_newline ft () - | Ppdir_print_flush -> Format.pp_print_flush ft () - in - fun (dirstream : _ ppdirs) -> - try - Glue.iter pp_dir dirstream - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = Format.pp_print_flush ft () in - Exninfo.iraise reraise - -(* pretty printing functions WITHOUT FLUSH *) -let pp_with ?pp_tag ft strm = - pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm)) - -(* pretty printing functions WITH FLUSH *) -let msg_with ?pp_tag ft strm = - pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) + try pp_cmd + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + let () = Format.pp_print_flush ft () in + Exninfo.iraise reraise (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch them to different windows. *) (** Output to a string formatter *) -let string_of_ppcmds c = - Format.fprintf Format.str_formatter "@[%a@]" (msg_with ?pp_tag:None) c; +let string_of_ppcmds ?pp_tag c = + Format.fprintf Format.str_formatter "@[%a@]" (pp_with ?pp_tag) c; Format.flush_str_formatter () (* Copy paste from Util *) @@ -310,7 +250,7 @@ let pr_nth n = (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) -let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Glue.empty l +let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Ppcmd_empty l (* unlike all other functions below, [prlist] works lazily. if a strict behavior is needed, use [prlist_strict] instead. -- cgit v1.2.3 From 77b61ac3de351f462f113f8075c11518b2847935 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:10:22 +0200 Subject: [pp] Make pp public to allow serialization. --- lib/pp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 6d7bdf75e3..140ad4e222 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -19,14 +19,14 @@ open Pp_control \end{description} *) +type pp_tag = string list + type block_type = | Pp_hbox of int | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int -type pp_tag = string list - type std_ppcmds = | Ppcmd_empty | Ppcmd_string of string -- cgit v1.2.3 From 689893ab0b648c8385ce77ec47127676088fccd5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 01:53:29 +0200 Subject: [pp] Implement n-ary glue. --- lib/pp.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 140ad4e222..405fe0f86f 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -30,7 +30,7 @@ type block_type = type std_ppcmds = | Ppcmd_empty | Ppcmd_string of string - | Ppcmd_glue of std_ppcmds * std_ppcmds + | Ppcmd_glue of std_ppcmds list | Ppcmd_box of block_type * std_ppcmds | Ppcmd_print_break of int * int | Ppcmd_white_space of int @@ -80,7 +80,7 @@ let utf8_length s = let app s1 s2 = match s1, s2 with | Ppcmd_empty, s | s, Ppcmd_empty -> s - | s1, s2 -> Ppcmd_glue(s1, s2) + | s1, s2 -> Ppcmd_glue [s1; s2] let (++) = app @@ -109,7 +109,7 @@ let strbrk s = 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 List.fold_left (++) Ppcmd_empty (aux 0 0) + in Ppcmd_glue (aux 0 0) let pr_loc_pos loc = if Loc.is_ghost loc then (str"") @@ -187,7 +187,7 @@ let pp_with ?pp_tag ft = in let rec pp_cmd = let open Format in function | Ppcmd_empty -> () - | Ppcmd_glue(s1,s2) -> pp_cmd s1; pp_cmd s2 + | Ppcmd_glue sl -> List.iter pp_cmd sl | Ppcmd_string str -> let n = utf8_length str in pp_print_as ft n str | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) @@ -250,7 +250,7 @@ let pr_nth n = (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) -let prlist pr l = List.fold_left (fun x e -> x ++ pr e) Ppcmd_empty l +let prlist pr l = Ppcmd_glue (List.map pr l) (* unlike all other functions below, [prlist] works lazily. if a strict behavior is needed, use [prlist_strict] instead. -- cgit v1.2.3 From 6c521565323ae8af22fb03e65664ef944da6ecdf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 17:12:11 +0200 Subject: [pp] Force well-tagged docs by construction. We replace open/close tag commands by a well-balanced "tag" wrapper. --- lib/pp.ml | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 405fe0f86f..4ff10b4d72 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -38,8 +38,7 @@ type std_ppcmds = | Ppcmd_open_box of block_type | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_open_tag of pp_tag - | Ppcmd_close_tag + | Ppcmd_tag of pp_tag * std_ppcmds (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) @@ -146,9 +145,7 @@ let hovb n = Ppcmd_open_box(Pp_hovbox n) let close () = Ppcmd_close_box (* Opening and closed of tags *) -let open_tag t = Ppcmd_open_tag t -let close_tag () = Ppcmd_close_tag -let tag t s = open_tag t ++ s ++ close_tag () +let tag t s = Ppcmd_tag(t,s) (* In new syntax only double quote char is escaped by repeating it *) let escape_string s = @@ -200,16 +197,9 @@ let pp_with ?pp_tag ft = | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms - | Ppcmd_open_tag tag -> - begin match pp_tag with - | None -> () - | Some f -> Format.pp_open_tag ft (f tag) - end - | Ppcmd_close_tag -> - begin match pp_tag with - | None -> () - | Some _ -> Format.pp_close_tag ft () - end + | Ppcmd_tag(tag, s) -> Option.iter (fun f -> pp_open_tag ft (f tag)) pp_tag; + pp_cmd s; + Option.iter (fun _ -> pp_close_tag ft () ) pp_tag in try pp_cmd with reraise -> -- cgit v1.2.3 From fd6271089a0f0fcaa6d89e347d76247c7c831d23 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 19:44:13 +0200 Subject: [pp] Force well-formed boxes by construction. We replace open/close box commands in favor of the create box ones. --- lib/pp.ml | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 4ff10b4d72..388eed9e45 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -32,13 +32,12 @@ type std_ppcmds = | Ppcmd_string of string | Ppcmd_glue of std_ppcmds list | Ppcmd_box of block_type * std_ppcmds + | Ppcmd_tag of pp_tag * std_ppcmds + (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_white_space of int | Ppcmd_force_newline - | Ppcmd_open_box of block_type - | Ppcmd_close_box | Ppcmd_comment of string list - | Ppcmd_tag of pp_tag * std_ppcmds (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) @@ -137,13 +136,6 @@ let v n s = Ppcmd_box(Pp_vbox n,s) let hv n s = Ppcmd_box(Pp_hvbox n,s) let hov n s = Ppcmd_box(Pp_hovbox n,s) -(* Opening and closing of boxes *) -let hb n = Ppcmd_open_box(Pp_hbox n) -let vb n = Ppcmd_open_box(Pp_vbox n) -let hvb n = Ppcmd_open_box(Pp_hvbox n) -let hovb n = Ppcmd_open_box(Pp_hovbox n) -let close () = Ppcmd_close_box - (* Opening and closed of tags *) let tag t s = Ppcmd_tag(t,s) @@ -191,8 +183,6 @@ let pp_with ?pp_tag ft = cpp_open_box bty ; if not (Format.over_max_boxes ()) then pp_cmd ss; Format.pp_close_box ft () - | Ppcmd_open_box bty -> cpp_open_box bty - | Ppcmd_close_box -> pp_close_box ft () | Ppcmd_white_space n -> pp_print_break ft n 0 | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () -- cgit v1.2.3 From 7440be4ffaf6ace5b8e94354c9a56462f45fa2dd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 19:45:32 +0200 Subject: [pp] Remove redundant white spacing pp construct. --- lib/pp.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 388eed9e45..d763767dc2 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -35,7 +35,6 @@ type std_ppcmds = | Ppcmd_tag of pp_tag * std_ppcmds (* Are those redundant? *) | Ppcmd_print_break of int * int - | Ppcmd_white_space of int | Ppcmd_force_newline | Ppcmd_comment of string list @@ -86,7 +85,7 @@ let (++) = app let str s = Ppcmd_string s let brk (a,b) = Ppcmd_print_break (a,b) let fnl () = Ppcmd_force_newline -let ws n = Ppcmd_white_space n +let ws n = Ppcmd_print_break (n,0) let comment l = Ppcmd_comment l (* derived commands *) @@ -183,7 +182,6 @@ let pp_with ?pp_tag ft = cpp_open_box bty ; if not (Format.over_max_boxes ()) then pp_cmd ss; Format.pp_close_box ft () - | Ppcmd_white_space n -> pp_print_break ft n 0 | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms -- cgit v1.2.3 From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:30:21 +0200 Subject: [pp] Make feedback the only logging mechanism. Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent. --- lib/pp.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index d763767dc2..5dba0356d8 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp_control - (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -178,10 +176,9 @@ let pp_with ?pp_tag ft = | Ppcmd_glue sl -> List.iter pp_cmd sl | Ppcmd_string str -> let n = utf8_length str in pp_print_as ft n str - | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - cpp_open_box bty ; - if not (Format.over_max_boxes ()) then pp_cmd ss; - Format.pp_close_box ft () + | Ppcmd_box(bty,ss) -> cpp_open_box bty ; + if not (over_max_boxes ()) then pp_cmd ss; + pp_close_box ft () | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms -- cgit v1.2.3 From a8ec2dc5c330ded1ba400ef202c57e68d2533312 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 18:17:46 +0100 Subject: [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. --- lib/pp.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 5dba0356d8..53c1fb4c31 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -17,7 +17,7 @@ \end{description} *) -type pp_tag = string list +type pp_tag = string type block_type = | Pp_hbox of int @@ -161,10 +161,8 @@ let rec pr_com ft s = Some s2 -> Format.pp_force_newline ft (); pr_com ft s2 | None -> () -type tag_handler = pp_tag -> Format.tag - (* pretty printing functions *) -let pp_with ?pp_tag ft = +let pp_with ft = let cpp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n @@ -182,9 +180,9 @@ let pp_with ?pp_tag ft = | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms - | Ppcmd_tag(tag, s) -> Option.iter (fun f -> pp_open_tag ft (f tag)) pp_tag; + | Ppcmd_tag(tag, s) -> pp_open_tag ft tag; pp_cmd s; - Option.iter (fun _ -> pp_close_tag ft () ) pp_tag + pp_close_tag ft () in try pp_cmd with reraise -> @@ -197,8 +195,8 @@ let pp_with ?pp_tag ft = them to different windows. *) (** Output to a string formatter *) -let string_of_ppcmds ?pp_tag c = - Format.fprintf Format.str_formatter "@[%a@]" (pp_with ?pp_tag) c; +let string_of_ppcmds c = + Format.fprintf Format.str_formatter "@[%a@]" pp_with c; Format.flush_str_formatter () (* Copy paste from Util *) -- cgit v1.2.3 From 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 17:56:22 +0100 Subject: [pp] Move terminal-specific tagging to the toplevel. Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`. --- lib/pp.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 53c1fb4c31..7b21f9bbd9 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -288,4 +288,3 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v let prvect elem v = prvect_with_sep mt elem v let surround p = hov 1 (str"(" ++ p ++ str")") - -- cgit v1.2.3 From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Dec 2016 12:12:54 +0100 Subject: [pp] [ide] Minor cleanups in pp code. - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics. --- lib/pp.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 7b21f9bbd9..80c599274a 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -77,6 +77,8 @@ let app s1 s2 = match s1, s2 with | s, Ppcmd_empty -> s | s1, s2 -> Ppcmd_glue [s1; s2] +let seq s = Ppcmd_glue s + let (++) = app (* formatting commands *) -- cgit v1.2.3 From fb04bc5cae0d648c379b9eb44f8b515f8e15b854 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 17 Mar 2017 18:12:03 +0100 Subject: [pp] Hide the internal representation of `std_ppcmds`. Following a suggestion by @ppedrot in #390, we require `Pp` clients to be aware that they are using a "view" on the `std_ppcmds` type. This is not extremely useful as people caring about the documents will indeed have to follow changes in the view, but it costs little to play on the safe side here for now. We also introduce a more standard notation, `Pp.t` for the main type. --- lib/pp.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'lib/pp.ml') diff --git a/lib/pp.ml b/lib/pp.ml index 80c599274a..9f33756dfe 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -25,17 +25,25 @@ type block_type = | Pp_hvbox of int | Pp_hovbox of int -type std_ppcmds = +type doc_view = | Ppcmd_empty | Ppcmd_string of string - | Ppcmd_glue of std_ppcmds list - | Ppcmd_box of block_type * std_ppcmds - | Ppcmd_tag of pp_tag * std_ppcmds + | Ppcmd_glue of doc_view list + | Ppcmd_box of block_type * doc_view + | Ppcmd_tag of pp_tag * doc_view (* Are those redundant? *) | Ppcmd_print_break of int * int | Ppcmd_force_newline | Ppcmd_comment of string list +(* Following discussion on #390, we play on the safe side and make the + internal representation opaque here. *) +type t = doc_view +type std_ppcmds = t + +let repr x = x +let unrepr x = x + (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) Rem 2 : if used for an iso8859_1 encoded string, the result is -- cgit v1.2.3