--- a/src/Pure/Concurrent/future.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 11 22:55:47 2011 +0200
@@ -117,7 +117,7 @@
val ok =
(case the (Single_Assignment.peek result) of
Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
- | Exn.Result _ => true);
+ | Exn.Res _ => true);
in ok end;
@@ -482,7 +482,7 @@
val task = Task_Queue.dummy_task ();
val group = Task_Queue.group_of_task task;
val result = Single_Assignment.var "value" : 'a result;
- val _ = assign_result group result (Exn.Result x);
+ val _ = assign_result group result (Exn.Res x);
in Future {promised = false, task = task, result = result} end;
fun map_future f x =
@@ -544,7 +544,7 @@
else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
in () end;
-fun fulfill x res = fulfill_result x (Exn.Result res);
+fun fulfill x res = fulfill_result x (Exn.Res res);
(* cancellation *)
--- a/src/Pure/Concurrent/lazy_sequential.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML Mon Jul 11 22:55:47 2011 +0200
@@ -23,7 +23,7 @@
| Result res => SOME res);
fun lazy e = Lazy (Unsynchronized.ref (Expr e));
-fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
(* force result *)
--- a/src/Pure/Concurrent/single_assignment.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Mon Jul 11 22:55:47 2011 +0200
@@ -38,7 +38,7 @@
(case peek v of
NONE =>
(case Multithreading.sync_wait NONE NONE cond lock of
- Exn.Result _ => wait ()
+ Exn.Res _ => wait ()
| Exn.Exn exn => reraise exn)
| SOME x => x);
in wait () end);
--- a/src/Pure/Concurrent/synchronized.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Mon Jul 11 22:55:47 2011 +0200
@@ -47,8 +47,8 @@
(case f x of
NONE =>
(case Multithreading.sync_wait NONE (time_limit x) cond lock of
- Exn.Result true => try_change ()
- | Exn.Result false => NONE
+ Exn.Res true => try_change ()
+ | Exn.Res false => NONE
| Exn.Exn exn => reraise exn)
| SOME (y, x') =>
uninterruptible (fn _ => fn () =>
--- a/src/Pure/General/exn.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/General/exn.ML Mon Jul 11 22:55:47 2011 +0200
@@ -1,13 +1,13 @@
(* Title: Pure/General/exn.ML
Author: Makarius
-Extra support for exceptions.
+Support for exceptions.
*)
signature EXN =
sig
- datatype 'a result = Result of 'a | Exn of exn
- val get_result: 'a result -> 'a option
+ datatype 'a result = Res of 'a | Exn of exn
+ val get_res: 'a result -> 'a option
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
@@ -33,24 +33,24 @@
(* runtime exceptions as values *)
datatype 'a result =
- Result of 'a |
+ Res of 'a |
Exn of exn;
-fun get_result (Result x) = SOME x
- | get_result _ = NONE;
+fun get_res (Res x) = SOME x
+ | get_res _ = NONE;
fun get_exn (Exn exn) = SOME exn
| get_exn _ = NONE;
-fun capture f x = Result (f x) handle e => Exn e;
+fun capture f x = Res (f x) handle e => Exn e;
-fun release (Result y) = y
+fun release (Res y) = y
| release (Exn e) = reraise e;
-fun flat_result (Result x) = x
+fun flat_result (Res x) = x
| flat_result (Exn e) = Exn e;
-fun map_result f (Result x) = Result (f x)
+fun map_result f (Res x) = Res (f x)
| map_result f (Exn e) = Exn e;
fun maps_result f = flat_result o map_result f;
@@ -72,7 +72,7 @@
| is_interrupt_exn _ = false;
fun interruptible_capture f x =
- Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
+ Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
(* nested exceptions *)
@@ -84,8 +84,8 @@
and flatten_list exns = List.concat (map flatten exns);
fun release_all results =
- if List.all (fn Result _ => true | _ => false) results
- then map (fn Result x => x) results
+ if List.all (fn Res _ => true | _ => false) results
+ then map (fn Res x => x) results
else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
fun release_first results = release_all results
--- a/src/Pure/General/exn.scala Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/General/exn.scala Mon Jul 11 22:55:47 2011 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/General/exn.scala
Author: Makarius
-Extra support for exceptions (arbitrary throwables).
+Support for exceptions (arbitrary throwables).
*/
package isabelle
--- a/src/Pure/Isar/proof.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jul 11 22:55:47 2011 +0200
@@ -1008,8 +1008,8 @@
|> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
|> int ? (fn goal_state =>
(case test_proof goal_state of
- Exn.Result (SOME _) => goal_state
- | Exn.Result NONE => error (fail_msg (context_of goal_state))
+ Exn.Res (SOME _) => goal_state
+ | Exn.Res NONE => error (fail_msg (context_of goal_state))
| Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
--- a/src/Pure/Isar/runtime.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Isar/runtime.ML Mon Jul 11 22:55:47 2011 +0200
@@ -101,7 +101,7 @@
fun debugging f x =
if ! debug then
Exn.release (exception_trace (fn () =>
- Exn.Result (f x) handle
+ Exn.Res (f x) handle
exn as UNDEF => Exn.Exn exn
| exn as EXCURSION_FAIL _ => Exn.Exn exn))
else f x;
--- a/src/Pure/ML-Systems/multithreading.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML Mon Jul 11 22:55:47 2011 +0200
@@ -55,7 +55,7 @@
fun with_attributes _ e = e [];
-fun sync_wait _ _ _ _ = Exn.Result true;
+fun sync_wait _ _ _ _ = Exn.Res true;
(* tracing *)
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Mon Jul 11 22:55:47 2011 +0200
@@ -97,8 +97,8 @@
(sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
(fn _ =>
(case time of
- SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
- | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
+ SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
+ | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
handle exn => Exn.Exn exn);
--- a/src/Pure/ML/install_pp_polyml-5.3.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml-5.3.ML Mon Jul 11 22:55:47 2011 +0200
@@ -14,13 +14,13 @@
(case Future.peek x of
NONE => PolyML.PrettyString "<future>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
+ | SOME (Exn.Res y) => pretty (y, depth)));
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
(case Lazy.peek x of
NONE => PolyML.PrettyString "<lazy>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
+ | SOME (Exn.Res y) => pretty (y, depth)));
PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
let
--- a/src/Pure/ML/install_pp_polyml.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/ML/install_pp_polyml.ML Mon Jul 11 22:55:47 2011 +0200
@@ -9,12 +9,12 @@
(case Future.peek x of
NONE => str "<future>"
| SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
+ | SOME (Exn.Res y) => print (y, depth)));
PolyML.install_pp
(fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
(case Lazy.peek x of
NONE => str "<lazy>"
| SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Result y) => print (y, depth)));
+ | SOME (Exn.Res y) => print (y, depth)));
--- a/src/Pure/PIDE/document.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/PIDE/document.ML Mon Jul 11 22:55:47 2011 +0200
@@ -252,8 +252,8 @@
val path = Path.explode thy_name;
val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
- | NONE => Exn.Result raw_tr) of
- Exn.Result tr =>
+ | NONE => Exn.Res raw_tr) of
+ Exn.Res tr =>
let
val is_init = is_some (Toplevel.init_of tr);
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
--- a/src/Pure/Syntax/syntax_phases.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Jul 11 22:55:47 2011 +0200
@@ -197,7 +197,7 @@
(* decode_term -- transform parse tree into raw term *)
fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
- | decode_term ctxt (reports0, Exn.Result tm) =
+ | decode_term ctxt (reports0, Exn.Res tm) =
let
fun get_const a =
((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
@@ -259,7 +259,7 @@
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
+fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
@@ -361,7 +361,7 @@
else [];
(*brute-force disambiguation via type-inference*)
- fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
+ fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
handle exn as ERROR _ => Exn.Exn exn;
val results' =
--- a/src/Pure/System/invoke_scala.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML Mon Jul 11 22:55:47 2011 +0200
@@ -48,7 +48,7 @@
val result =
(case tag of
"0" => Exn.Exn Null
- | "1" => Exn.Result res
+ | "1" => Exn.Res res
| "2" => Exn.Exn (ERROR res)
| "3" => Exn.Exn (Fail res)
| _ => raise Fail "Bad tag");
--- a/src/Pure/proofterm.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/proofterm.ML Mon Jul 11 22:55:47 2011 +0200
@@ -217,7 +217,7 @@
else
let val seen' = Inttab.update (i, ()) seen in
(case Future.peek body of
- SOME (Exn.Result body') => status body' (st, seen')
+ SOME (Exn.Res body') => status body' (st, seen')
| SOME (Exn.Exn _) =>
let val (oracle, unfinished, _) = st
in ((oracle, unfinished, true), seen') end
--- a/src/Pure/thm.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Pure/thm.ML Mon Jul 11 22:55:47 2011 +0200
@@ -528,7 +528,7 @@
let
val ps = map (Future.peek o snd) promises;
val bodies = body ::
- map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+ map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
val {oracle, unfinished, failed} = Proofterm.status_of bodies;
in
{oracle = oracle,
--- a/src/Tools/quickcheck.ML Mon Jul 11 22:50:29 2011 +0200
+++ b/src/Tools/quickcheck.ML Mon Jul 11 22:55:47 2011 +0200
@@ -237,9 +237,9 @@
if Config.get ctxt quiet then
try tester v
else
- let
+ let (* FIXME !?!? *)
val tester = Exn.interruptible_capture tester v
- in case Exn.get_result tester of
+ in case Exn.get_res tester of
NONE => SOME (Exn.release tester)
| SOME tester => SOME tester
end