author | wenzelm |
Wed, 13 Aug 2014 13:57:55 +0200 | |
changeset 57927 | f14c1248d064 |
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;