output_words_as : (int * num -> radix) -> unit
STRUCTURE
wordsLib
SYNOPSIS
Controls pretty-printing of word literals.
DESCRIPTION
A call to output_words_as f makes function f determine the output base for word literals. The funtion f takes a word-length/word-value pair and returns the required output radix.
EXAMPLE
The default setting is: 
output_words_as
  (fn (l, v) =>
      if Arbnum.<= (Arbnum.fromHexString "10000", v)
         then StringCvt.HEX
      else StringCvt.DEC);
The l = 0 case is used for word literals with non-numeric index types. 
- wordsLib.output_words_as
    (fn (l,_) => if l = 0 then StringCvt.HEX else StringCvt.DEC);
- ``32w``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``0x20w`` : term
- ``32w:word5``;
> val it = ``32w`` : term
COMMENTS
Printing and parsing in octal is controlled by the reference base_tokens.allow_octal_input. Pretty-printing for word literals can be turned off with a call to wordsLib.output_words_as_dec.
SEEALSO
add_user_printer, output_words_as_dec, output_words_as_bin, output_words_as_oct, output_words_as_hex
HOL  Kananaskis-9