(* constants and types that are influenced
   by the actual printer : *)
const
  f_len = 120;
      (* length of a format-string *)

  max_right_margin = 1920; (* 80 x 24 points *)
      (* maximum value for right margin in the formatted document *)

  min_width = 48; (* 2 x 24 points *)
      (* minimum distance between left margin and right margin
         in the formatted document *)

  min_line_spacing = 1;  (* point *)
  max_line_spacing = 85; (* point *)
      (* minimum and maximum value for line spacing *)

  char_height = 10; (* points *)
      (* the height of one character *)

  forced_space = #10;
      (* this character is used for "forced spaces" which will
         not be suppressed by the formatting process *)

type
  attribute = ((* typefaces and modifiers to them : *)
                 bold, italic, proportional,
                 nlq, unidirectional,
                 underscore, subscript, superscript,
               (* used by the formatting process : *)
                 dividepoint, space);
               (* note: in addition to the two above, also
                  underscore is used by the formatting process.
                  It is assumed that underscoring a character
                  does not change its width. *)