merged
authorwenzelm
Mon Jul 11 23:20:40 2011 +0200 (2011-07-11)
changeset 4376524b8244d672b
parent 43764 366d5726de09
parent 43763 ab11dcfa3e6d
child 43766 9545bb3cefac
merged
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jul 11 18:44:58 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jul 11 23:20:40 2011 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4      val ok =
     1.5        (case the (Single_Assignment.peek result) of
     1.6          Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
     1.7 -      | Exn.Result _ => true);
     1.8 +      | Exn.Res _ => true);
     1.9    in ok end;
    1.10  
    1.11  
    1.12 @@ -482,7 +482,7 @@
    1.13      val task = Task_Queue.dummy_task ();
    1.14      val group = Task_Queue.group_of_task task;
    1.15      val result = Single_Assignment.var "value" : 'a result;
    1.16 -    val _ = assign_result group result (Exn.Result x);
    1.17 +    val _ = assign_result group result (Exn.Res x);
    1.18    in Future {promised = false, task = task, result = result} end;
    1.19  
    1.20  fun map_future f x =
    1.21 @@ -544,7 +544,7 @@
    1.22          else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
    1.23      in () end;
    1.24  
    1.25 -fun fulfill x res = fulfill_result x (Exn.Result res);
    1.26 +fun fulfill x res = fulfill_result x (Exn.Res res);
    1.27  
    1.28  
    1.29  (* cancellation *)
     2.1 --- a/src/Pure/Concurrent/lazy_sequential.ML	Mon Jul 11 18:44:58 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/lazy_sequential.ML	Mon Jul 11 23:20:40 2011 +0200
     2.3 @@ -23,7 +23,7 @@
     2.4    | Result res => SOME res);
     2.5  
     2.6  fun lazy e = Lazy (Unsynchronized.ref (Expr e));
     2.7 -fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
     2.8 +fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
     2.9  
    2.10  
    2.11  (* force result *)
     3.1 --- a/src/Pure/Concurrent/single_assignment.ML	Mon Jul 11 18:44:58 2011 +0200
     3.2 +++ b/src/Pure/Concurrent/single_assignment.ML	Mon Jul 11 23:20:40 2011 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4          (case peek v of
     3.5            NONE =>
     3.6              (case Multithreading.sync_wait NONE NONE cond lock of
     3.7 -              Exn.Result _ => wait ()
     3.8 +              Exn.Res _ => wait ()
     3.9              | Exn.Exn exn => reraise exn)
    3.10          | SOME x => x);
    3.11      in wait () end);
     4.1 --- a/src/Pure/Concurrent/synchronized.ML	Mon Jul 11 18:44:58 2011 +0200
     4.2 +++ b/src/Pure/Concurrent/synchronized.ML	Mon Jul 11 23:20:40 2011 +0200
     4.3 @@ -47,8 +47,8 @@
     4.4            (case f x of
     4.5              NONE =>
     4.6                (case Multithreading.sync_wait NONE (time_limit x) cond lock of
     4.7 -                Exn.Result true => try_change ()
     4.8 -              | Exn.Result false => NONE
     4.9 +                Exn.Res true => try_change ()
    4.10 +              | Exn.Res false => NONE
    4.11                | Exn.Exn exn => reraise exn)
    4.12            | SOME (y, x') =>
    4.13                uninterruptible (fn _ => fn () =>
     5.1 --- a/src/Pure/General/exn.ML	Mon Jul 11 18:44:58 2011 +0200
     5.2 +++ b/src/Pure/General/exn.ML	Mon Jul 11 23:20:40 2011 +0200
     5.3 @@ -1,13 +1,13 @@
     5.4  (*  Title:      Pure/General/exn.ML
     5.5      Author:     Makarius
     5.6  
     5.7 -Extra support for exceptions.
     5.8 +Support for exceptions.
     5.9  *)
    5.10  
    5.11  signature EXN =
    5.12  sig
    5.13 -  datatype 'a result = Result of 'a | Exn of exn
    5.14 -  val get_result: 'a result -> 'a option
    5.15 +  datatype 'a result = Res of 'a | Exn of exn
    5.16 +  val get_res: 'a result -> 'a option
    5.17    val get_exn: 'a result -> exn option
    5.18    val capture: ('a -> 'b) -> 'a -> 'b result
    5.19    val release: 'a result -> 'a
    5.20 @@ -33,24 +33,24 @@
    5.21  (* runtime exceptions as values *)
    5.22  
    5.23  datatype 'a result =
    5.24 -  Result of 'a |
    5.25 +  Res of 'a |
    5.26    Exn of exn;
    5.27  
    5.28 -fun get_result (Result x) = SOME x
    5.29 -  | get_result _ = NONE;
    5.30 +fun get_res (Res x) = SOME x
    5.31 +  | get_res _ = NONE;
    5.32  
    5.33  fun get_exn (Exn exn) = SOME exn
    5.34    | get_exn _ = NONE;
    5.35  
    5.36 -fun capture f x = Result (f x) handle e => Exn e;
    5.37 +fun capture f x = Res (f x) handle e => Exn e;
    5.38  
    5.39 -fun release (Result y) = y
    5.40 +fun release (Res y) = y
    5.41    | release (Exn e) = reraise e;
    5.42  
    5.43 -fun flat_result (Result x) = x
    5.44 +fun flat_result (Res x) = x
    5.45    | flat_result (Exn e) = Exn e;
    5.46  
    5.47 -fun map_result f (Result x) = Result (f x)
    5.48 +fun map_result f (Res x) = Res (f x)
    5.49    | map_result f (Exn e) = Exn e;
    5.50  
    5.51  fun maps_result f = flat_result o map_result f;
    5.52 @@ -72,7 +72,7 @@
    5.53    | is_interrupt_exn _ = false;
    5.54  
    5.55  fun interruptible_capture f x =
    5.56 -  Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
    5.57 +  Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
    5.58  
    5.59  
    5.60  (* nested exceptions *)
    5.61 @@ -84,8 +84,8 @@
    5.62  and flatten_list exns = List.concat (map flatten exns);
    5.63  
    5.64  fun release_all results =
    5.65 -  if List.all (fn Result _ => true | _ => false) results
    5.66 -  then map (fn Result x => x) results
    5.67 +  if List.all (fn Res _ => true | _ => false) results
    5.68 +  then map (fn Res x => x) results
    5.69    else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
    5.70  
    5.71  fun release_first results = release_all results
     6.1 --- a/src/Pure/General/exn.scala	Mon Jul 11 18:44:58 2011 +0200
     6.2 +++ b/src/Pure/General/exn.scala	Mon Jul 11 23:20:40 2011 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  /*  Title:      Pure/General/exn.scala
     6.5      Author:     Makarius
     6.6  
     6.7 -Extra support for exceptions (arbitrary throwables).
     6.8 +Support for exceptions (arbitrary throwables).
     6.9  */
    6.10  
    6.11  package isabelle
    6.12 @@ -12,8 +12,8 @@
    6.13    /* runtime exceptions as values */
    6.14  
    6.15    sealed abstract class Result[A]
    6.16 -  case class Res[A](val result: A) extends Result[A]
    6.17 -  case class Exn[A](val exn: Throwable) extends Result[A]
    6.18 +  case class Res[A](res: A) extends Result[A]
    6.19 +  case class Exn[A](exn: Throwable) extends Result[A]
    6.20  
    6.21    def capture[A](e: => A): Result[A] =
    6.22      try { Res(e) }
     7.1 --- a/src/Pure/General/output.ML	Mon Jul 11 18:44:58 2011 +0200
     7.2 +++ b/src/Pure/General/output.ML	Mon Jul 11 23:20:40 2011 +0200
     7.3 @@ -96,9 +96,8 @@
     7.4    val prompt_fn = Unsynchronized.ref raw_stdout;
     7.5    val status_fn = Unsynchronized.ref (fn _: output => ());
     7.6    val report_fn = Unsynchronized.ref (fn _: output => ());
     7.7 -  val raw_message_fn =
     7.8 -    Unsynchronized.ref
     7.9 -      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
    7.10 +  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    7.11 +    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
    7.12  end;
    7.13  
    7.14  fun writeln s = ! Private_Hooks.writeln_fn (output s);
     8.1 --- a/src/Pure/Isar/proof.ML	Mon Jul 11 18:44:58 2011 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Mon Jul 11 23:20:40 2011 +0200
     8.3 @@ -1008,8 +1008,8 @@
     8.4      |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
     8.5      |> int ? (fn goal_state =>
     8.6        (case test_proof goal_state of
     8.7 -        Exn.Result (SOME _) => goal_state
     8.8 -      | Exn.Result NONE => error (fail_msg (context_of goal_state))
     8.9 +        Exn.Res (SOME _) => goal_state
    8.10 +      | Exn.Res NONE => error (fail_msg (context_of goal_state))
    8.11        | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
    8.12    end;
    8.13  
     9.1 --- a/src/Pure/Isar/runtime.ML	Mon Jul 11 18:44:58 2011 +0200
     9.2 +++ b/src/Pure/Isar/runtime.ML	Mon Jul 11 23:20:40 2011 +0200
     9.3 @@ -101,7 +101,7 @@
     9.4  fun debugging f x =
     9.5    if ! debug then
     9.6      Exn.release (exception_trace (fn () =>
     9.7 -      Exn.Result (f x) handle
     9.8 +      Exn.Res (f x) handle
     9.9          exn as UNDEF => Exn.Exn exn
    9.10        | exn as EXCURSION_FAIL _ => Exn.Exn exn))
    9.11    else f x;
    10.1 --- a/src/Pure/ML-Systems/multithreading.ML	Mon Jul 11 18:44:58 2011 +0200
    10.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Mon Jul 11 23:20:40 2011 +0200
    10.3 @@ -55,7 +55,7 @@
    10.4  
    10.5  fun with_attributes _ e = e [];
    10.6  
    10.7 -fun sync_wait _ _ _ _ = Exn.Result true;
    10.8 +fun sync_wait _ _ _ _ = Exn.Res true;
    10.9  
   10.10  
   10.11  (* tracing *)
    11.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jul 11 18:44:58 2011 +0200
    11.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jul 11 23:20:40 2011 +0200
    11.3 @@ -97,8 +97,8 @@
    11.4      (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
    11.5      (fn _ =>
    11.6        (case time of
    11.7 -        SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
    11.8 -      | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
    11.9 +        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
   11.10 +      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
   11.11        handle exn => Exn.Exn exn);
   11.12  
   11.13  
    12.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML	Mon Jul 11 18:44:58 2011 +0200
    12.2 +++ b/src/Pure/ML/install_pp_polyml-5.3.ML	Mon Jul 11 23:20:40 2011 +0200
    12.3 @@ -14,13 +14,13 @@
    12.4    (case Future.peek x of
    12.5      NONE => PolyML.PrettyString "<future>"
    12.6    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    12.7 -  | SOME (Exn.Result y) => pretty (y, depth)));
    12.8 +  | SOME (Exn.Res y) => pretty (y, depth)));
    12.9  
   12.10  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   12.11    (case Lazy.peek x of
   12.12      NONE => PolyML.PrettyString "<lazy>"
   12.13    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   12.14 -  | SOME (Exn.Result y) => pretty (y, depth)));
   12.15 +  | SOME (Exn.Res y) => pretty (y, depth)));
   12.16  
   12.17  PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
   12.18    let
    13.1 --- a/src/Pure/ML/install_pp_polyml.ML	Mon Jul 11 18:44:58 2011 +0200
    13.2 +++ b/src/Pure/ML/install_pp_polyml.ML	Mon Jul 11 23:20:40 2011 +0200
    13.3 @@ -9,12 +9,12 @@
    13.4      (case Future.peek x of
    13.5        NONE => str "<future>"
    13.6      | SOME (Exn.Exn _) => str "<failed>"
    13.7 -    | SOME (Exn.Result y) => print (y, depth)));
    13.8 +    | SOME (Exn.Res y) => print (y, depth)));
    13.9  
   13.10  PolyML.install_pp
   13.11    (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
   13.12      (case Lazy.peek x of
   13.13        NONE => str "<lazy>"
   13.14      | SOME (Exn.Exn _) => str "<failed>"
   13.15 -    | SOME (Exn.Result y) => print (y, depth)));
   13.16 +    | SOME (Exn.Res y) => print (y, depth)));
   13.17  
    14.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 11 18:44:58 2011 +0200
    14.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 11 23:20:40 2011 +0200
    14.3 @@ -252,8 +252,8 @@
    14.4              val path = Path.explode thy_name;
    14.5              val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
    14.6            in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
    14.7 -      | NONE => Exn.Result raw_tr) of
    14.8 -    Exn.Result tr =>
    14.9 +      | NONE => Exn.Res raw_tr) of
   14.10 +    Exn.Res tr =>
   14.11        let
   14.12          val is_init = is_some (Toplevel.init_of tr);
   14.13          val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    15.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon Jul 11 18:44:58 2011 +0200
    15.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Jul 11 23:20:40 2011 +0200
    15.3 @@ -197,7 +197,7 @@
    15.4  (* decode_term -- transform parse tree into raw term *)
    15.5  
    15.6  fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
    15.7 -  | decode_term ctxt (reports0, Exn.Result tm) =
    15.8 +  | decode_term ctxt (reports0, Exn.Res tm) =
    15.9        let
   15.10          fun get_const a =
   15.11            ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
   15.12 @@ -259,7 +259,7 @@
   15.13  
   15.14  fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
   15.15  
   15.16 -fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
   15.17 +fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
   15.18  fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
   15.19  
   15.20  fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
   15.21 @@ -361,7 +361,7 @@
   15.22              else [];
   15.23  
   15.24            (*brute-force disambiguation via type-inference*)
   15.25 -          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
   15.26 +          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
   15.27              handle exn as ERROR _ => Exn.Exn exn;
   15.28  
   15.29            val results' =
    16.1 --- a/src/Pure/System/invoke_scala.ML	Mon Jul 11 18:44:58 2011 +0200
    16.2 +++ b/src/Pure/System/invoke_scala.ML	Mon Jul 11 23:20:40 2011 +0200
    16.3 @@ -48,7 +48,7 @@
    16.4      val result =
    16.5        (case tag of
    16.6          "0" => Exn.Exn Null
    16.7 -      | "1" => Exn.Result res
    16.8 +      | "1" => Exn.Res res
    16.9        | "2" => Exn.Exn (ERROR res)
   16.10        | "3" => Exn.Exn (Fail res)
   16.11        | _ => raise Fail "Bad tag");
    17.1 --- a/src/Pure/library.scala	Mon Jul 11 18:44:58 2011 +0200
    17.2 +++ b/src/Pure/library.scala	Mon Jul 11 23:20:40 2011 +0200
    17.3 @@ -20,14 +20,19 @@
    17.4  {
    17.5    /* user errors */
    17.6  
    17.7 +  private val runtime_exception = Class.forName("java.lang.RuntimeException")
    17.8 +
    17.9    object ERROR
   17.10    {
   17.11      def apply(message: String): Throwable = new RuntimeException(message)
   17.12      def unapply(exn: Throwable): Option[String] =
   17.13        exn match {
   17.14          case e: RuntimeException =>
   17.15 -          val msg = e.getMessage
   17.16 -          Some(if (msg == null) "Error" else msg)
   17.17 +          if (e.getClass != runtime_exception) Some(e.toString)
   17.18 +          else {
   17.19 +            val msg = e.getMessage
   17.20 +            Some(if (msg == null) "Error" else msg)
   17.21 +          }
   17.22          case _ => None
   17.23        }
   17.24    }
    18.1 --- a/src/Pure/proofterm.ML	Mon Jul 11 18:44:58 2011 +0200
    18.2 +++ b/src/Pure/proofterm.ML	Mon Jul 11 23:20:40 2011 +0200
    18.3 @@ -217,7 +217,7 @@
    18.4              else
    18.5                let val seen' = Inttab.update (i, ()) seen in
    18.6                  (case Future.peek body of
    18.7 -                  SOME (Exn.Result body') => status body' (st, seen')
    18.8 +                  SOME (Exn.Res body') => status body' (st, seen')
    18.9                  | SOME (Exn.Exn _) =>
   18.10                      let val (oracle, unfinished, _) = st
   18.11                      in ((oracle, unfinished, true), seen') end
    19.1 --- a/src/Pure/thm.ML	Mon Jul 11 18:44:58 2011 +0200
    19.2 +++ b/src/Pure/thm.ML	Mon Jul 11 23:20:40 2011 +0200
    19.3 @@ -528,7 +528,7 @@
    19.4    let
    19.5      val ps = map (Future.peek o snd) promises;
    19.6      val bodies = body ::
    19.7 -      map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
    19.8 +      map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
    19.9      val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   19.10    in
   19.11     {oracle = oracle,
    20.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Jul 11 18:44:58 2011 +0200
    20.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Jul 11 23:20:40 2011 +0200
    20.3 @@ -214,37 +214,33 @@
    20.4              r2 <- r1.try_restrict(chunk_range)
    20.5            } yield r2
    20.6  
    20.7 +        val padded_markup =
    20.8 +          if (markup.isEmpty)
    20.9 +            Iterator(Text.Info(chunk_range, None))
   20.10 +          else
   20.11 +            Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
   20.12 +            markup.iterator ++
   20.13 +            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
   20.14 +
   20.15          var x1 = x + w
   20.16          gfx.setFont(chunk_font)
   20.17 -        if (markup.isEmpty) {
   20.18 -          gfx.setColor(chunk_color)
   20.19 -          gfx.drawString(chunk.str, x1, y)
   20.20 -        }
   20.21 -        else {
   20.22 -          for {
   20.23 -            Text.Info(range, info) <-
   20.24 -              Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
   20.25 -              markup.iterator ++
   20.26 -              Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
   20.27 -            if !range.is_singularity
   20.28 -          } {
   20.29 -            val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   20.30 -            gfx.setColor(info.getOrElse(chunk_color))
   20.31 +        for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
   20.32 +          val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
   20.33 +          gfx.setColor(info.getOrElse(chunk_color))
   20.34  
   20.35 -            range.try_restrict(caret_range) match {
   20.36 -              case Some(r) if !r.is_singularity =>
   20.37 -                val astr = new AttributedString(str)
   20.38 -                val i = r.start - range.start
   20.39 -                val j = r.stop - range.start
   20.40 -                astr.addAttribute(TextAttribute.FONT, chunk_font)
   20.41 -                astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
   20.42 -                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
   20.43 -                gfx.drawString(astr.getIterator, x1, y)
   20.44 -              case _ =>
   20.45 -                gfx.drawString(str, x1, y)
   20.46 -            }
   20.47 -            x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
   20.48 +          range.try_restrict(caret_range) match {
   20.49 +            case Some(r) if !r.is_singularity =>
   20.50 +              val astr = new AttributedString(str)
   20.51 +              val i = r.start - range.start
   20.52 +              val j = r.stop - range.start
   20.53 +              astr.addAttribute(TextAttribute.FONT, chunk_font)
   20.54 +              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
   20.55 +              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
   20.56 +              gfx.drawString(astr.getIterator, x1, y)
   20.57 +            case _ =>
   20.58 +              gfx.drawString(str, x1, y)
   20.59            }
   20.60 +          x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
   20.61          }
   20.62        }
   20.63        w += chunk.width
    21.1 --- a/src/Tools/quickcheck.ML	Mon Jul 11 18:44:58 2011 +0200
    21.2 +++ b/src/Tools/quickcheck.ML	Mon Jul 11 23:20:40 2011 +0200
    21.3 @@ -237,9 +237,9 @@
    21.4      if Config.get ctxt quiet then
    21.5        try tester v
    21.6      else
    21.7 -      let
    21.8 +      let (* FIXME !?!? *)
    21.9          val tester = Exn.interruptible_capture tester v
   21.10 -      in case Exn.get_result tester of
   21.11 +      in case Exn.get_res tester of
   21.12            NONE => SOME (Exn.release tester)
   21.13          | SOME tester => SOME tester
   21.14        end