#4377: sizedText function for Text.PrettyPrint
---------------------------------+------------------------------------------
Reporter: lerkok | Owner:
Type: feature request | Status: new
Priority: normal | Component: libraries/pretty
Version: | Keywords: text, sizedText, pretty
printing, Text.PrettyPrint
Testcase: | Blockedby:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4377>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
