src/Pure/General/exn.ML

prefer Exn.result: avoid accidental capture of interrupts, similar to ML;

(*  Title:      Pure/General/exn.ML
    Author:     Makarius

Support for exceptions.
*)

signature BASIC_EXN =
sig
  exception ERROR of string
  val error: string -> 'a
  val cat_error: string -> string -> 'a
end;

signature EXN0 =
sig
  include BASIC_EXN
  val polyml_location: exn -> PolyML.location option
  val reraise: exn -> 'a
  datatype 'a result = Res of 'a | Exn of exn
  val is_res: 'a result -> bool
  val is_exn: 'a result -> bool
  val get_res: 'a result -> 'a option
  val get_exn: 'a result -> exn option
  val capture0: ('a -> 'b) -> 'a -> 'b result  (*unmanaged interrupts*)
  val release: 'a result -> 'a
  val map_res: ('a -> 'b) -> 'a result -> 'b result
  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
  val map_exn: (exn -> exn) -> 'a result -> 'a result
  val cause: exn -> exn
  exception Interrupt_Break
  exception Interrupt_Breakdown
  val is_interrupt_raw: exn -> bool
  val is_interrupt_break: exn -> bool
  val is_interrupt_breakdown: exn -> bool
  val is_interrupt_proper: exn -> bool
  val is_interrupt: exn -> bool
  val is_interrupt_proper_exn: 'a result -> bool
  val is_interrupt_exn: 'a result -> bool
  val result: ('a -> 'b) -> 'a -> 'b result
  val failure_rc: exn -> int
  exception EXCEPTIONS of exn list
  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
end;

signature EXN =
sig
  include EXN0
  val capture: ('a -> 'b) -> 'a -> 'b result  (*managed interrupts*)
  val capture_body: (unit -> 'a) -> 'a result
end;

structure Exn: EXN0 =
struct

(* location *)

val polyml_location = PolyML.Exception.exceptionLocation;

val reraise = PolyML.Exception.reraise;


(* user errors *)

exception ERROR of string;

fun error msg = raise ERROR msg;

fun cat_error "" msg = error msg
  | cat_error msg "" = error msg
  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);


(* exceptions as values *)

datatype 'a result =
  Res of 'a |
  Exn of exn;

fun is_res (Res _) = true
  | is_res _ = false;

fun is_exn (Exn _) = true
  | is_exn _ = false;

fun get_res (Res x) = SOME x
  | get_res _ = NONE;

fun get_exn (Exn exn) = SOME exn
  | get_exn _ = NONE;

fun capture0 f x = Res (f x) handle e => Exn e;

fun release (Res y) = y
  | release (Exn e) = reraise e;

fun map_res f (Res x) = Res (f x)
  | map_res f (Exn e) = Exn e;

fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;

fun map_exn f (Res x) = Res x
  | map_exn f (Exn e) = Exn (f e);


(* interrupts *)

fun cause (IO.Io {cause = exn, ...}) = cause exn
  | cause exn = exn;

exception Interrupt_Break;
exception Interrupt_Breakdown;

fun is_interrupt_raw exn = (case cause exn of Thread.Thread.Interrupt => true | _ => false);
fun is_interrupt_break exn = (case cause exn of Interrupt_Break => true | _ => false);
fun is_interrupt_breakdown exn = (case cause exn of Interrupt_Breakdown => true | _ => false);
fun is_interrupt_proper exn = is_interrupt_raw exn orelse is_interrupt_break exn;
fun is_interrupt exn = is_interrupt_proper exn orelse is_interrupt_breakdown exn;

fun is_interrupt_proper_exn (Exn exn) = is_interrupt_proper exn
  | is_interrupt_proper_exn _ = false;

fun is_interrupt_exn (Exn exn) = is_interrupt exn
  | is_interrupt_exn _ = false;

fun result f x =
  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;

fun failure_rc exn = if is_interrupt exn then 130 else 2;


(* concatenated exceptions *)

exception EXCEPTIONS of exn list;


(* low-level trace *)

fun trace exn_message output e =
  PolyML.Exception.traceException
    (e, fn (trace, exn) =>
      let
        val title = "Exception trace - " ^ exn_message exn;
        val () = output (String.concatWith "\n" (title :: trace));
      in reraise exn end);

end;