Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007862OCamlstandard librarypublic2018-10-09 09:442018-11-09 17:32
Assigned To 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007862: Possible bug in Format
DescriptionThe second call to "print_space" in "Steps To Reproduce" generates a trailing space even though the line is broken. Moreover, removing either

  print_string "qyyyyyyyy";
  print_space ();


  open_box 0;
  close_box ();

results in "correct" behavior (the line is not broken).
Steps To Reproduceopen Format
let () =
  open_box 0;
  print_string "qyyyyyyyy";
  print_space ();
  print_string "qzzzzzzzzzzzzzzzzzzzqzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzfffaaq";
  print_space ();
  open_box 0;
  close_box ();
  print_string "q";
  close_box ()
Additional InformationOutput (there is a trailing space in the second line):

TagsNo tags attached.
Attached Files

- Relationships
related to 0007807new Format: More refined check to evaluate whether a box shall lead to go beyond max_indent and need a break prior to opening? 

-  Notes
frisch (developer)
2018-10-09 09:48

Note that the doc says:

  [pp_print_space ppf ()] emits a 'space' break hint:
  the pretty-printer may split the line at this point,
  otherwise it prints one space.

which indeed suggests that the expected behavior is that the space should not be printed when the pretty-printer does split the line (and this is what usually happens).
bvaugon (developer)
2018-10-09 10:53
edited on: 2018-10-09 10:58

It seems that there is two problems: an "unwanted trailing space" and a "suprising line break".

Concerning the "surprising line break" that is automatically inserted by the open_box once the current line size exceed 68 characters (68 = default_margin - default_min_space_left), it is configurable through the "min_space_left" property:

  (* Minimal space left before margin, when opening a box. *)
  mutable pp_min_space_left : int;

using the Format.set_max_indent function :

set_max_indent 77;

where max_indent = margin - space_left.

Remarks that calling pp_set_max_indent with an argument greater or equal than margin has no effect.

frisch (developer)
2018-10-09 11:21

I think the only problem here is the unwanted trailing space.
nojebar (developer)
2018-10-09 11:24

I am not sure about that, because if I remove the code that prints the first line, then there is no break between second and third line, which tells me that there is enough space and a break is not warranted there.

In other words: maybe the trailing space is correct and the problem is the break that shouldn't happen.
bvaugon (developer)
2018-10-09 12:24

In fact, when you remove the code that prints the first line, there is no break but it should be (or the documentation should be fixed). Indeed, opening a box after the 68th character should not be allowed following the comment "pp_min_space_left: minimal space left before margin when opening a box".

Furthermore (I don't know if there is a link with the other problems), opening a box at this positions seems to break vertical alignement like in the text printed by the following code:

open Format;
let () =
  open_box 0;
  print_string "q";
  print_space ();
  print_string "qzzzzzzzzzzzzzzzzzzzqzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzfffaaa";
  print_space ();
  open_vbox 0;
  print_string "A";
  print_space ();
  print_string "B";
  close_box ();
  print_space ();
  print_string "q";
  close_box ();


q qzzzzzzzzzzzzzzzzzzzqzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzfffaaa A
                                                                    B q

A and B should be aligned.
octachron (developer)
2018-10-10 13:28
edited on: 2018-10-10 13:29

This is due to the current behavior of max_indent: it rejects to the left boxes opened beyond max_indent (if the enclosing box does not fit on the line). In particular, it does not try to understand if the opened box could fit on the line, see 0007807 .

bvaugon, for your second example, this is due to the fact that max_indent limits the maximum indentation of the value.

frisch (developer)
2018-11-09 13:58

Guys, do you think the only "problem" is the overly preventive heuristics mentioned in 0007807, and that using a more clever approach there would avoid all cases where pp_print_space currently prints a space even though the line is broken?
octachron (developer)
2018-11-09 17:32

I am not sure for all cases, but a better integration of the max_indent limit or a way to disable it would solve this specific issue.

- Issue History
Date Modified Username Field Change
2018-10-09 09:44 nojebar New Issue
2018-10-09 09:48 frisch Note Added: 0019405
2018-10-09 10:53 bvaugon Note Added: 0019406
2018-10-09 10:58 bvaugon Note Edited: 0019406 View Revisions
2018-10-09 11:21 frisch Note Added: 0019407
2018-10-09 11:24 nojebar Note Added: 0019408
2018-10-09 12:24 bvaugon Note Added: 0019409
2018-10-10 13:28 octachron Note Added: 0019410
2018-10-10 13:29 octachron Note Edited: 0019410 View Revisions
2018-10-10 13:29 octachron Note Edited: 0019410 View Revisions
2018-10-10 13:29 octachron Relationship added related to 0007807
2018-11-09 13:58 frisch Note Added: 0019437
2018-11-09 17:32 octachron Note Added: 0019449

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker