author | wenzelm |
Sat, 23 May 2015 17:19:37 +0200 | |
changeset 60299 | 5ae2a2e74c93 |
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;