Commits on Nov 8, 2020

1. Reformulate wrapping in terms of boxes, glue, and penalties …

   This is a complete rewrite of the core word wrapping functionality.
   Before, we would step though the input string and (attempt to) keep
   track of all aspects of the state. This didn't always work (see at
   least #122, #158, #158, and #193) and it's inflexible.
   
   This commit replaces the old algorithm with a new one which works on a
   more abstract level. We now first
   
   1. First split the input string into "words". A word is a substring of
      the original string, including any trailing whitespace.
   
   2. We split each word according to the `WordSplitter`.
   
   3. We then simply put the words into lines based on the display width.
   
   This is slower than the previous algorithm. The `fill/1600` benchmark
   shows that is now takes ~18 microseconds to wrap a 1600 character long
   string. That is around 8 microseconds longer than before.

   

   mgeisler committed Nov 8, 2020
   Configuration menu

   • View commit details
   • Copy full SHA for 1fc0ba3
   • Browse repository at this point

   Copy the full SHA

   1fc0ba3 View commit details

   Browse the repository at this point in the history