--- a/src/Pure/ML/exn_output_polyml.ML Wed Feb 17 23:06:24 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title: Pure/ML/exn_output_polyml.ML
- Author: Makarius
-
-Auxiliary operations for exception output -- Poly/ML version.
-*)
-
-signature EXN_OUTPUT =
-sig
- val position: exn -> Position.T
- val pretty: exn -> Pretty.T
-end;
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position exn =
- (case PolyML.exceptionLocation exn of
- NONE => Position.none
- | SOME loc => Exn_Properties.position_of loc);
-
-fun pretty (exn: exn) =
- Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
-
-end;