1(* Title: Pure/General/exn.ML 2 Author: Makarius 3 4Support for exceptions. 5*) 6 7structure Exn: Exn = 8struct 9 10(* location *) 11 12val polyml_location = PolyML.Exception.exceptionLocation; 13 14val reraise = PolyML.Exception.reraise; 15 16 17(* user errors *) 18 19exception ERROR of string; 20 21fun error msg = raise ERROR msg; 22 23fun cat_error "" msg = error msg 24 | cat_error msg "" = error msg 25 | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2); 26 27 28(* exceptions as values *) 29 30datatype 'a result = 31 Res of 'a | 32 Exn of exn; 33 34fun get_res (Res x) = SOME x 35 | get_res _ = NONE; 36 37fun get_exn (Exn exn) = SOME exn 38 | get_exn _ = NONE; 39 40fun capture f x = Res (f x) handle e => Exn e; 41 42fun release (Res y) = y 43 | release (Exn e) = reraise e; 44 45fun map_res f (Res x) = Res (f x) 46 | map_res f (Exn e) = Exn e; 47 48fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f; 49 50fun map_exn f (Res x) = Res x 51 | map_exn f (Exn e) = Exn (f e); 52 53 54(* interrupts *) 55 56exception Interrupt = Thread.Thread.Interrupt; 57 58fun interrupt () = raise Interrupt; 59 60fun is_interrupt Interrupt = true 61 | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause 62 | is_interrupt _ = false; 63 64val interrupt_exn = Exn Interrupt; 65 66fun is_interrupt_exn (Exn exn) = is_interrupt exn 67 | is_interrupt_exn _ = false; 68 69fun interruptible_capture f x = 70 Res (f x) handle e => if is_interrupt e then reraise e else Exn e; 71 72 73(* concatenated exceptions *) 74 75exception EXCEPTIONS of exn list; 76 77 78(* low-level trace *) 79 80fun trace exn_message output e = 81 PolyML.Exception.traceException 82 (e, fn (trace, exn) => 83 let 84 val title = "Exception trace - " ^ exn_message exn; 85 val () = output (String.concatWith "\n" (title :: trace)); 86 in reraise exn end); 87 88end; 89