src/Pure/ML-Systems/exn.ML
author wenzelm
Tue, 21 Jul 2009 20:24:02 +0200
changeset 32100 8ac6b1102f16
parent 31427 5a07cc86675d
permissions -rw-r--r--
added flatten/flatten_list -- supercedes internal plain_exns; represent empty failure as EXCEPTIONS [] instead of Interrupt;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/exn.ML
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
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
     4
Extra 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
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
     9
  datatype 'a result = Exn of exn | Result of 'a
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    10
  val get_result: 'a result -> 'a option
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
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    14
  exception Interrupt
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    15
  exception EXCEPTIONS of exn list
32100
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    16
  val flatten: exn -> exn list
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    17
  val flatten_list: exn list -> exn list
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    18
  val release_all: 'a result list -> 'a list
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    19
  val release_first: 'a result list -> 'a list
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    20
end;
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    21
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    22
structure Exn: EXN =
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    23
struct
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    24
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    25
(* runtime exceptions as values *)
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    26
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    27
datatype 'a result =
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    28
  Result of 'a |
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    29
  Exn of exn;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    30
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    31
fun get_result (Result x) = SOME x
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    32
  | get_result _ = NONE;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    33
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    34
fun get_exn (Exn exn) = SOME exn
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    35
  | get_exn _ = NONE;
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 capture f x = Result (f x) handle e => Exn e;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    38
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    39
fun release (Result y) = y
31427
5a07cc86675d reraise exceptions to preserve original position (ML system specific);
wenzelm
parents: 29564
diff changeset
    40
  | release (Exn e) = reraise e;
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    41
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    42
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    43
(* interrupt and nested exceptions *)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    44
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    45
exception Interrupt = Interrupt;
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    46
exception EXCEPTIONS of exn list;
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    47
32100
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    48
fun flatten Interrupt = []
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    49
  | flatten (EXCEPTIONS exns) = flatten_list exns
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    50
  | flatten exn = [exn]
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    51
and flatten_list exns = List.concat (map flatten exns);
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    52
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    53
fun release_all results =
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    54
  if List.all (fn Result _ => true | _ => false) results
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    55
  then map (fn Result x => x) results
32100
8ac6b1102f16 added flatten/flatten_list -- supercedes internal plain_exns;
wenzelm
parents: 31427
diff changeset
    56
  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    57
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    58
fun release_first results = release_all results
31427
5a07cc86675d reraise exceptions to preserve original position (ML system specific);
wenzelm
parents: 29564
diff changeset
    59
  handle EXCEPTIONS (exn :: _) => reraise exn;
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    60
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    61
end;