[isabelle-dev] [PATCH 1 of 1] Fix top-level printing of exception messages containing forced-line breaks

[Makarius]

On Tue, 2 Apr 2013, David Greenaway wrote:

> # HG changeset patch
> # User David Greenaway <david.greenaway at nicta.com.au>
> # Date 1364864695 -39600
> # Node ID 27bd348e777a3ffa4a4bf5bb18faa0a8428e468f
> # Parent  d40aec502416a0eaa094e5aef1f317f7c4867852
> Fix top-level printing of exception messages containing forced-line breaks.
> 
> Both Isabelle and PolyML have pretty printers. One problem arises when
> converting from Isabelle's format to PolyML's format, in that the former
> supports "forced line breaks" while the latter does not. The current solution
> is to expand such line-breaks into a large number of spaces (99999, to be
> precise), preventing PolyML from fitting the spaces on a line, and hence
> forcing it to produce a line-break.
> 
> This approach, unfortunately, falls down in two areas: "PolyML.makestring"
> renders the large amount of spaces, producing undesirable results. Similarly,
> "General.exnMessage" in PolyML simply calls "PolyML.makestring", and hence has
> the same problem.
> 
> The problem can be seen with the following testcase:
>
>     definition "test a b ≡ undefined"
>     notation (output) test ("test // (_) // (_)")
>     ML {* raise (CTERM ("test", [@{cterm "test x y" }])) *}
> 
> This patch fixes one instance of this problem by using an alternative mechanism
> to pretty-print unhanded exceptions which prevents the large number of spaces
> being rendered.
> 
> diff --git a/src/Pure/Isar/runtime.ML b/src/Pure/Isar/runtime.ML
> --- a/src/Pure/Isar/runtime.ML
> +++ b/src/Pure/Isar/runtime.ML
> @@ -65,6 +65,10 @@
>          SOME exns => maps (flatten context) exns
>        | NONE => [(context, identify exn)]);
> 
> +fun str_of_exn (exn : exn) =
> +  PolyML.prettyRepresentation (exn, ! Pretty.margin_default)
> +  |> pretty_ml |> Pretty.from_ML |> Pretty.string_of

Sorry, I did not mean to re-open this messy thread anytime soon, but David 
Matthews had offered his help with forced breaks in Poly/ML in privite 
mail.  Since I did not want to waste his time as well, I've looked through 
the situation in Isabelle/ML once more, eventually resulting in 
http://isabelle.in.tum.de/repos/isabelle/rev/b7f908c99546

Doing this, I cross-checked with the above proposal, just as part of the 
normal professional routine, despite all the annoyances caused on this 
mailing list.

This revealed a genuine "bug" in the change, one of the rare sort that are 
easily pointed out: "! Pretty.margin_default" should be "get_print_depth ()"
as can be seen from existing uses of this function, e.g. here 
http://isabelle.in.tum.de/repos/isabelle/file/b7f908c99546/src/Pure/ML-Systems/polyml.ML#l160


"This patch fixes ..." nothing, it introduces a subtle bug that could 
easily take years to rediscover.  I don't want to blame anybody.  And I am 
not repeating anything I've tried to explain earlier on this (and related) 
threads.  I just hope that lessons are learned eventually.

This is why we have this mailing list: to learn how things are done 
properly, despite all the challenges caused by this sophisticated system.

[Thread closed, as far as I am concerned.]


 	Makarius