On Tue, 2 Apr 2013, David Greenaway wrote:
# HG changeset patch
# User David Greenaway <[email protected]>
# 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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
