src/Pure/ML-Systems/exn.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 29564 f8b933a62151
child 31427 5a07cc86675d
permissions -rw-r--r--
more modular setup of runtime compilation;
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
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    16
  val release_all: 'a result list -> 'a list
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    17
  val release_first: 'a result list -> 'a list
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    18
end;
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    19
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    20
structure Exn: EXN =
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    21
struct
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    22
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    23
(* runtime exceptions as values *)
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    24
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    25
datatype 'a result =
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    26
  Result of 'a |
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    27
  Exn of exn;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    28
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    29
fun get_result (Result x) = SOME x
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    30
  | get_result _ = NONE;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    31
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    32
fun get_exn (Exn exn) = SOME exn
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    33
  | get_exn _ = NONE;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    34
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    35
fun capture f x = Result (f x) handle e => Exn e;
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 release (Result y) = y
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    38
  | release (Exn e) = raise e;
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    39
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    40
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    41
(* interrupt and nested exceptions *)
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    42
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    43
exception Interrupt = Interrupt;
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    44
exception EXCEPTIONS of exn list;
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    45
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    46
fun plain_exns (Result _) = []
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    47
  | plain_exns (Exn Interrupt) = []
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    48
  | plain_exns (Exn (EXCEPTIONS exns)) = List.concat (map (plain_exns o Exn) exns)
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    49
  | plain_exns (Exn exn) = [exn];
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    50
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    51
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    52
fun release_all results =
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    53
  if List.all (fn Result _ => true | _ => false) results
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    54
  then map (fn Result x => x) results
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    55
  else
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    56
    (case List.concat (map plain_exns results) of
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    57
      [] => raise Interrupt
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    58
    | exns => raise EXCEPTIONS exns);
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    59
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    60
fun release_first results = release_all results
28459
f6a4d913cfb1 simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm
parents: 28444
diff changeset
    61
  handle EXCEPTIONS (exn :: _) => raise exn;
28444
283d5e41953d more robust treatment of Interrupt;
wenzelm
parents: 23962
diff changeset
    62
23962
e0358fac0541 Runtime exceptions as values (from library.ML);
wenzelm
parents:
diff changeset
    63
end;