adapted Susp.peek;
authorwenzelm
Thu Oct 23 13:52:28 2008 +0200 (2008-10-23)
changeset 286720baf1d9c6780
parent 28671 ed6681dd35d8
child 28673 d746a8c12c43
adapted Susp.peek;
src/Pure/Isar/code.ML
src/Pure/ML-Systems/install_pp_polyml.ML
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 23 13:52:27 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 23 13:52:28 2008 +0200
     1.3 @@ -118,12 +118,12 @@
     1.4  (* defining equations with linear flag, default flag and lazy theorems *)
     1.5  
     1.6  fun pretty_lthms ctxt r = case Susp.peek r
     1.7 - of SOME thms => map (ProofContext.pretty_thm ctxt o fst) thms
     1.8 + of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
     1.9    | NONE => [Pretty.str "[...]"];
    1.10  
    1.11  fun certificate thy f r =
    1.12    case Susp.peek r
    1.13 -   of SOME thms => (Susp.value o f thy) thms
    1.14 +   of SOME thms => (Susp.value o f thy) (Exn.release thms)
    1.15      | NONE => let
    1.16          val thy_ref = Theory.check_thy thy;
    1.17        in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
     2.1 --- a/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 13:52:27 2008 +0200
     2.2 +++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 23 13:52:28 2008 +0200
     2.3 @@ -13,4 +13,6 @@
     2.4  install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
     2.5    (case Susp.peek x of
     2.6      NONE => str "<delayed>"
     2.7 -  | SOME y => print (y, depth)));
     2.8 +  | SOME (Exn.Exn _) => str "<failed>"
     2.9 +  | SOME (Exn.Result y) => print (y, depth)));
    2.10 +