author | wenzelm |
Thu, 30 Oct 2014 22:45:19 +0100 | |
changeset 58839 | ccda99401bc8 |
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;