diff options
| author | Hugo Herbelin | 2020-10-05 22:21:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-08 23:47:14 +0200 |
| commit | db278921c54201a01543953cc0986fc0fb126615 (patch) | |
| tree | 70115f7e9365b34c4464affbb9a8cf71a925317c /ide/coqide/protocol/xmlprotocol.ml | |
| parent | e18ed350f7b5710c382ea1306e7b1e7e2fb0c9f8 (diff) | |
Dropping the misleading int argument of Pp.h.
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
Diffstat (limited to 'ide/coqide/protocol/xmlprotocol.ml')
| -rw-r--r-- | ide/coqide/protocol/xmlprotocol.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index 56a934b8d4..9e861baac6 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -103,14 +103,14 @@ let to_routeid = function let of_routeid i = Element ("route_id",["val",string_of_int i],[]) let of_box (ppb : Pp.block_type) = let open Pp in match ppb with - | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_hbox -> constructor "ppbox" "hbox" [] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] let to_box = let open Pp in do_match "ppbox" (fun s args -> match s with - | "hbox" -> Pp_hbox (to_int (singleton args)) + | "hbox" -> empty args; Pp_hbox | "vbox" -> Pp_vbox (to_int (singleton args)) | "hvbox" -> Pp_hvbox (to_int (singleton args)) | "hovbox" -> Pp_hovbox (to_int (singleton args)) |