src/Pure/General/exn.ML
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 78764 a3dcae9a2ebe
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62508
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents: 62505
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
62491
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
     7
signature BASIC_EXN =
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
     8
sig
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
     9
  exception ERROR of string
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
    10
  val error: string -> 'a
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
    11
  val cat_error: string -> string -> 'a
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
    12
end;
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
    13
78715
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    14
signature EXN0 =
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    15
sig
62491
7187cb7a77c5 clarified modules;
wenzelm
parents: 62198
diff changeset
    16
  include BASIC_EXN
62821
48c24d0b6d85 tuned signature;
wenzelm
parents: 62508
diff changeset
    17
  val polyml_location: exn -> PolyML.location option
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
    18
  val reraise: exn -> 'a
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    19
  datatype 'a result = Res of 'a | Exn of exn
78674
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    20
  val is_res: 'a result -> bool
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    21
  val is_exn: 'a result -> bool
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    22
  val get_res: 'a result -> 'a option
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    23
  val get_exn: 'a result -> exn option
78715
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    24
  val capture0: ('a -> 'b) -> 'a -> 'b result  (*unmanaged interrupts*)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    25
  val release: 'a result -> 'a
61077
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
    26
  val map_res: ('a -> 'b) -> 'a result -> 'b result
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
    27
  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
    28
  val map_exn: (exn -> exn) -> 'a result -> 'a result
78683
cde40295ffd6 clarified signature;
wenzelm
parents: 78681
diff changeset
    29
  val cause: exn -> exn
78764
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    30
  exception Interrupt_Break
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    31
  exception Interrupt_Breakdown
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    32
  val is_interrupt_raw: exn -> bool
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    33
  val is_interrupt_break: exn -> bool
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    34
  val is_interrupt_breakdown: exn -> bool
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    35
  val is_interrupt_proper: exn -> bool
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    36
  val is_interrupt: exn -> bool
78764
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
    37
  val is_interrupt_proper_exn: 'a result -> bool
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
    38
  val is_interrupt_exn: 'a result -> bool
78705
fde0b195cb7d clarified signature: avoid association with potentially dangerous Exn.capture;
wenzelm
parents: 78683
diff changeset
    39
  val result: ('a -> 'b) -> 'a -> 'b result
78673
90b12b919b5f clarified signature (again): follow Isabelle/Java/Scala;
wenzelm
parents: 78671
diff changeset
    40
  val failure_rc: exn -> int
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    41
  exception EXCEPTIONS of exn list
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
    42
  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    43
end;
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    44
78715
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    45
signature EXN =
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    46
sig
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    47
  include EXN0
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    48
  val capture: ('a -> 'b) -> 'a -> 'b result  (*managed interrupts*)
78757
a094bf81a496 clarified signature;
wenzelm
parents: 78715
diff changeset
    49
  val capture_body: (unit -> 'a) -> 'a result
78715
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    50
end;
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    51
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    52
structure Exn: EXN0 =
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    53
struct
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    54
62821
48c24d0b6d85 tuned signature;
wenzelm
parents: 62508
diff changeset
    55
(* location *)
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
    56
62821
48c24d0b6d85 tuned signature;
wenzelm
parents: 62508
diff changeset
    57
val polyml_location = PolyML.Exception.exceptionLocation;
48c24d0b6d85 tuned signature;
wenzelm
parents: 62508
diff changeset
    58
48c24d0b6d85 tuned signature;
wenzelm
parents: 62508
diff changeset
    59
val reraise = PolyML.Exception.reraise;
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
    60
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
    61
62492
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    62
(* user errors *)
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    63
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    64
exception ERROR of string;
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    65
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    66
fun error msg = raise ERROR msg;
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    67
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    68
fun cat_error "" msg = error msg
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    69
  | cat_error msg "" = error msg
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    70
  | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    71
0e53fade87fe clarified modules;
wenzelm
parents: 62491
diff changeset
    72
44158
fe6d1ae7a065 clarified Exn.message;
wenzelm
parents: 43761
diff changeset
    73
(* exceptions as values *)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    74
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    75
datatype 'a result =
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    76
  Res of 'a |
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    77
  Exn of exn;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    78
78674
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    79
fun is_res (Res _) = true
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    80
  | is_res _ = false;
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    81
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    82
fun is_exn (Exn _) = true
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    83
  | is_exn _ = false;
88f47c70187a clarified signature;
wenzelm
parents: 78673
diff changeset
    84
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    85
fun get_res (Res x) = SOME x
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    86
  | get_res _ = NONE;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    87
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    88
fun get_exn (Exn exn) = SOME exn
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    89
  | get_exn _ = NONE;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    90
78715
9506b852ebdf clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents: 78705
diff changeset
    91
fun capture0 f x = Res (f x) handle e => Exn e;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    92
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
    93
fun release (Res y) = y
31427
5a07cc86675d reraise exceptions to preserve original position (ML system specific);
wenzelm
parents: 29564
diff changeset
    94
  | release (Exn e) = reraise e;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    95
61077
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
    96
fun map_res f (Res x) = Res (f x)
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
    97
  | map_res f (Exn e) = Exn e;
42223
098c86e53153 more precise propagation of reports/results through some inner syntax layers;
wenzelm
parents: 40483
diff changeset
    98
61077
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
    99
fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
   100
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
   101
fun map_exn f (Res x) = Res x
06cca32aa519 thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents: 56667
diff changeset
   102
  | map_exn f (Exn e) = Exn (f e);
39472
1cf49add5b40 Exn.map_result
haftmann
parents: 39233
diff changeset
   103
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
   104
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
   105
(* interrupts *)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
   106
78683
cde40295ffd6 clarified signature;
wenzelm
parents: 78681
diff changeset
   107
fun cause (IO.Io {cause = exn, ...}) = cause exn
cde40295ffd6 clarified signature;
wenzelm
parents: 78681
diff changeset
   108
  | cause exn = exn;
cde40295ffd6 clarified signature;
wenzelm
parents: 78681
diff changeset
   109
78764
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   110
exception Interrupt_Break;
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   111
exception Interrupt_Breakdown;
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   112
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   113
fun is_interrupt_raw exn = (case cause exn of Thread.Thread.Interrupt => true | _ => false);
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   114
fun is_interrupt_break exn = (case cause exn of Interrupt_Break => true | _ => false);
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   115
fun is_interrupt_breakdown exn = (case cause exn of Interrupt_Breakdown => true | _ => false);
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   116
fun is_interrupt_proper exn = is_interrupt_raw exn orelse is_interrupt_break exn;
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   117
fun is_interrupt exn = is_interrupt_proper exn orelse is_interrupt_breakdown exn;
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   118
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   119
fun is_interrupt_proper_exn (Exn exn) = is_interrupt_proper exn
a3dcae9a2ebe distinguish proper interrupts from Poly/ML RTS breakdown;
wenzelm
parents: 78757
diff changeset
   120
  | is_interrupt_proper_exn _ = false;
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
   121
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
   122
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
   123
  | 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
   124
78705
fde0b195cb7d clarified signature: avoid association with potentially dangerous Exn.capture;
wenzelm
parents: 78683
diff changeset
   125
fun result f x =
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43537
diff changeset
   126
  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
   127
78673
90b12b919b5f clarified signature (again): follow Isabelle/Java/Scala;
wenzelm
parents: 78671
diff changeset
   128
fun failure_rc exn = if is_interrupt exn then 130 else 2;
90b12b919b5f clarified signature (again): follow Isabelle/Java/Scala;
wenzelm
parents: 78671
diff changeset
   129
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
   130
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 44246
diff changeset
   131
(* concatenated exceptions *)
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 34136
diff changeset
   132
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
   133
exception EXCEPTIONS of exn list;
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
   134
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   135
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   136
(* low-level trace *)
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   137
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   138
fun trace exn_message output e =
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   139
  PolyML.Exception.traceException
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   140
    (e, fn (trace, exn) =>
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   141
      let
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   142
        val title = "Exception trace - " ^ exn_message exn;
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   143
        val () = output (String.concatWith "\n" (title :: trace));
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   144
      in reraise exn end);
9e2a65912111 clarified modules;
wenzelm
parents: 62492
diff changeset
   145
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
   146
end;