| author | wenzelm |
| Sun, 30 Nov 2014 15:11:50 +0100 | |
| changeset 59069 | ec6ce25a630d |
| parent 56303 | 4cc3f4db3447 |
| child 62357 | ab76bd43c14a |
| permissions | -rw-r--r-- |
(* Title: Pure/ML/exn_output.ML Author: Makarius Auxiliary operations for exception output -- generic 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) = Position.none val pretty = Pretty.str o General.exnMessage; end;