author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
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;