Comment author: administrator

Full_Name: Benjamin Monate
Version: 3.07+2
OS: Linux
Submission from: is002447.saclay.cea.fr (132.166.134.145)

I have a problem with the following code :

open Format
set_tags true; printf "@{Hello@?@} World@\n"

This code outputs : "Hello World" without closing the BOLD tag.
Flushing the formatter seems to reset the formatter stack.
This does not seem to be documented.
Is this an intended behaviour or a bug ?

Thank you for your support
Benjamin

Thank you for your interesting bug report. The question you asked is
not so difficult to answer, since we have (from the doc):

1. ``@? : flush the pretty printer as with [print_flush ()].
2. ``val print_flush : unit -> unit;;
   (** Flushes the pretty printer: all opened boxes are closed,
   and all pending text is displayed. *)''
3. ``The behaviour of pretty-printing commands is unspecified
   if there is no opened pretty-printing box.''

From 1) and 2) we can conclude that no box is opened after evaluation
of ``@?'' in a format string. Now 3) easily gives us that the
behaviour of the commands in the rest of the format string is
unspecified.

Hence, the behaviour you observed is indeed consistent with the
documentation (whatever could have been this behaviour
anyway). Furthermore, since you do not open any pretty-printing box in
the entire format string, the printf call is entirely unspecified and
thus could have output nothing at all, or alternatively could have
been printing for ever random material from the computer's memory!

However, I agree with you that what you observed is not completely
satisfactory. So, I added 8 chars more to the Format module
implementation, so that the undefined'' behaviour of your undefined'' program is now:

set_tags true; printf "@{Hello@?@} World@\n";;

Hello World

• : unit
  =
  ()

You observe now that the toplevel formatting output is somewhat
disturbed by the effects of theunspecified'' program. In contrast, if we use @.'' in place of ``@\n'', we get a much better behaviour:

printf "@{Hello@?@} World@.";;

Hello World

• : unit = ()

In effect, we have (from the doc):

1. @\n: force a newline, as with [force_newline ()].
2. val force_newline : unit -> unit;;
   (** Forces a newline in the current box. Not the normal way of
   pretty-printing, you should prefer break hints. *)

meaning that @\n'' is not the normal way of pretty-printing''.

In conclusion: believe the doc and never use pretty-printing commands
out of boxes; also carefully avoid using ``@\n'', unless you really
know what you are doing :)

Thanks again for helping me to improve the Format module.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/

Comment author: administrator

Unspecified behavior, made more robust by PW 2004-02-11