Opened 5 years ago

Closed 5 years ago

#4377 closed proposal (fixed)

sizedText function for Text.PrettyPrint

Reported by: lerkok Owned by: simonmar
Priority: normal Milestone: Not GHC
Component: libraries/pretty Version:
Keywords: text, sizedText, pretty printing, Text.PrettyPrint Cc: Christian.Maeder@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The Text.PrettyPrint library has a text function for converting ordinary strings to documents. This function takes the length of the string to be its final size. However, there are use cases where the actual length of this string and the "virtual" length of the document it represents are not necessarily the same. This use case comes up in cases where the resulting "Doc" is rendered to String and a further processor works on that particular string with its own built-in assumptions about how things should be laid out. (In our case, we produce Isabelle/HOL code from Cryptol, which gets rendered by the Isabelle theorem prover. These strings are the tags that correspond to Isabelle's own escape sequences for certain theory specific logical symbols.)

To remedy this, adding a function "sizedText" to the library would suffice:

sizedText :: Int -> String -> Doc
sizedText l s = TextBeside (Str s') l Empty
   where s' = s ++ take (l - length s) (repeat ' ')

Unfortunately this function can not be defined outside the PrettyPrint library itself, This is because the TextBeside constructor is not exported, and there seems to be no other way of accessing the length field otherwise.

Note that in the above code the user given length l can be larger or smaller than the actual length of the string s; so the first argument to take can be positive or negative. In either case the function does the right thing for our use case: If smaller, you get the original string; which messes up the ASCII output a bit but is the right thing to the for the target processor; if larger, then it gets padded with space at the end appropriately to get the ASCII looking right as well.

Our current workaround for this issue is to replicate the library code ourselves and add this function on top, which is a kludge at best that we'd like to avoid.

The function sizedText satisfies the law:

    sizedText (length s) s = text s

and hence agrees with the existing text function for ordinary usage.

Attachments (1)

cleaned-up-and-added-sizedText.dpatch (32.9 KB) - added by maeder 5 years ago.
proposed darcs patches

Download all attachments as: .zip

Change History (11)

comment:1 Changed 5 years ago by lerkok

  • Type changed from feature request to proposal

The proposed sizedText function can also be viewed as a generalization of the already existing zeroWidthText function, except with arbitrary sizes not just 0. In this case we can define:

    zeroWidthText = sizedText 0

or just export sizedText to cover both use cases.

comment:2 Changed 5 years ago by maeder

  • Cc Christian.Maeder@… added

We copied the module, too, just to attach an arbitrary size to strings for LaTeX with proportional fonts and ligatures. So rather than padding a string I would rather attach any size to the given input string as is. (Padding can be added be the user). I don't see a use case for negative sizes, though, so these may be excluded (to ensure other invariants).

comment:3 Changed 5 years ago by lerkok

Thanks for the responses..

Looks like an appropriate definition would be:

sizedText :: Int -> String -> Doc
sizedText l s = textBeside_ (Str s) l Empty

Based on Thomas's suggestion to use textBeside_ and Christians suggestion that any padding should be done on the user side if necessary.

comment:4 Changed 5 years ago by igloo

  • Milestone set to Not GHC

comment:5 Changed 5 years ago by maeder

I had a look into the original file to suggest a patch for the above code, which misses one documenting haddock sentence and the adjusted export list.

However, the file contains trailing spaces, tabs, too long lines, redundant brackets and semicolons, etc.

Apart from replacing the definition of zeroWidthText, also the definition of indent (and spaces) should be replaced by (replicate ' '); multi_ch can be replaced by replicate.

I could create a couple of patches. To whom should I "darcs send" them? Or who would commit the changes. I suggest to bump the version to, since the interface is extended. (The addition of zeroWidthText changed the version from to, too)

Changed 5 years ago by maeder

proposed darcs patches

comment:6 Changed 5 years ago by maeder

  • Status changed from new to patch

The discussion thread started with and got two positive answers with suggestions for modifications that the proposer agreed to (above).

comment:7 Changed 5 years ago by lerkok

Christian: Thanks for taking the time to create this patch; it looks great to me and it would serve our needs over here at Galois.

comment:8 Changed 5 years ago by maeder

Could someone apply the patch then, please.

comment:9 Changed 5 years ago by simonmar

  • Owner set to simonmar

comment:10 Changed 5 years ago by simonmar

  • Resolution set to fixed
  • Status changed from patch to closed

Patches pushed, thanks:

Fri Dec 10 06:14:07 PST 2010  [email protected]
  * replaced tabs and removed trailing spaces

Fri Dec 10 08:13:02 PST 2010  [email protected]
  * added sizedText

Fri Dec 10 08:25:13 PST 2010  [email protected]
  * use replicate for indent, spaces and multi_ch

Fri Dec 10 08:44:47 PST 2010  [email protected]
  * shortened too long lines and removed redundant brackets
Note: See TracTickets for help on using tickets.