tuned signature -- corresponding to Scala version;

--- 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