src/Pure/General/exn.ML
author wenzelm
Wed, 17 Aug 2011 22:14:22 +0200
changeset 44247 270366301bd7
parent 44246 380a4677c55d
child 56628 a2df9de46060
permissions -rw-r--r--
more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents: 32100
diff changeset
     1
(*  Title:      Pure/General/exn.ML
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
     3
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
     4
Support for exceptions.
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
     5
*)
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
     6
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
     7
signature EXN =
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
     8
sig
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
     9
  datatype 'a result = Res of 'a | Exn of exn
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    10
  val get_res: 'a result -> 'a option
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    11
  val get_exn: 'a result -> exn option
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    12
  val capture: ('a -> 'b) -> 'a -> 'b result
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    13
  val release: 'a result -> 'a
40234
39af96cc57cb added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents: 39472
diff changeset
    14
  val map_result: ('a -> 'b) -> 'a result -> 'b result
42223
098c86e53153 more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents: 40483
diff changeset
    15
  val maps_result: ('a -> 'b result) -> 'a result -> 'b result
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    16
  exception Interrupt
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    17
  val interrupt: unit -> 'a
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    18
  val is_interrupt: exn -> bool
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    19
  val interrupt_exn: 'a result
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    20
  val is_interrupt_exn: 'a result -> bool
40234
39af96cc57cb added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents: 39472
diff changeset
    21
  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    22
  exception EXCEPTIONS of exn list
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    23
end;
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    24
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    25
structure Exn: EXN =
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    26
struct
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    27
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43761
diff changeset
    28
(* exceptions as values *)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    29
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    30
datatype 'a result =
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    31
  Res of 'a |
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    32
  Exn of exn;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    33
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    34
fun get_res (Res x) = SOME x
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    35
  | get_res _ = NONE;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    36
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    37
fun get_exn (Exn exn) = SOME exn
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    38
  | get_exn _ = NONE;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    39
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    40
fun capture f x = Res (f x) handle e => Exn e;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    41
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    42
fun release (Res y) = y
31427
5a07cc86675d reraise exceptions to preserve original position (ML system specific);
wenzelm
parents: 29564
diff changeset
    43
  | release (Exn e) = reraise e;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    44
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    45
fun map_result f (Res x) = Res (f x)
42223
098c86e53153 more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents: 40483
diff changeset
    46
  | map_result f (Exn e) = Exn e;
098c86e53153 more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents: 40483
diff changeset
    47
44246
380a4677c55d tuned signature;
wenzelm
parents: 44158
diff changeset
    48
fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
39472
1cf49add5b40 Exn.map_result
haftmann
parents: 39233
diff changeset
    49
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    50
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    51
(* interrupts *)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    52
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    53
exception Interrupt = Interrupt;
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    54
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    55
fun interrupt () = raise Interrupt;
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    56
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    57
fun is_interrupt Interrupt = true
40234
39af96cc57cb added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents: 39472
diff changeset
    58
  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    59
  | is_interrupt _ = false;
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    60
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    61
val interrupt_exn = Exn Interrupt;
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    62
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    63
fun is_interrupt_exn (Exn exn) = is_interrupt exn
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    64
  | is_interrupt_exn _ = false;
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    65
40234
39af96cc57cb added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents: 39472
diff changeset
    66
fun interruptible_capture f x =
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    67
  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
40234
39af96cc57cb added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release);
wenzelm
parents: 39472
diff changeset
    68
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    69
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 44246
diff changeset
    70
(* concatenated exceptions *)
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    71
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    72
exception EXCEPTIONS of exn list;
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    73
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    74
end;
40483
3848283c14bb treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm
parents: 40234
diff changeset
    75
3848283c14bb treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm
parents: 40234
diff changeset
    76
datatype illegal = Interrupt;
3848283c14bb treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm
parents: 40234
diff changeset
    77