# 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
+
in
fun exn_messages_ids exn_position e =
@@ -104,7 +108,7 @@
| THM (msg, i, thms) =>
raised exn ("THM " ^ string_of_int i)
(msg :: if_context context Display.string_of_thm thms)
- | _ => raised exn (General.exnMessage exn) []);
+ | _ => raised exn (str_of_exn exn) []);
in [((i, msg), id)] end)
and sorted_msgs context exn =
sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
