debug: exception_trace;
authorwenzelm
Wed Jul 06 20:00:41 2005 +0200 (2005-07-06 ago)
changeset 1672924c5c94aa967
parent 16728 c4c9d5df26ba
child 16730 ff304c52bf86
debug: exception_trace;
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jul 06 20:00:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jul 06 20:00:41 2005 +0200
     1.3 @@ -206,37 +206,49 @@
     1.4  fun copy_node true (Theory thy) = Theory (Theory.copy thy)
     1.5    | copy_node _ node = node;
     1.6  
     1.7 -fun interruptible f x =
     1.8 -  let val y = ref (NONE: node History.T option);
     1.9 -  in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end;
    1.10 -
    1.11 -val rollback = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
    1.12 +val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
    1.13  
    1.14  fun return (result, NONE) = result
    1.15    | return (result, SOME exn) = raise FAILURE (result, exn);
    1.16  
    1.17 +fun debug_trans f x =
    1.18 +  if ! debug then
    1.19 +    let val y = ref x in
    1.20 +      setmp Output.transform_exceptions false
    1.21 +        exception_trace (fn () => y := f x); ! y
    1.22 +    end
    1.23 +  else f x;
    1.24 +
    1.25 +fun interruptible f x =
    1.26 +  let val y = ref x
    1.27 +  in raise_interrupt (fn () => y := f x) (); ! y end;
    1.28 +
    1.29  in
    1.30  
    1.31  fun node_trans _ _ _ (State NONE) = raise UNDEF
    1.32    | node_trans int hist f (State (SOME (node, term))) =
    1.33        let
    1.34 -        fun mk_state nd = State (SOME (nd, term));
    1.35 -
    1.36          val cont_node = History.map (checkpoint_node int) node;
    1.37          val back_node = History.map (copy_node int) cont_node;
    1.38 +        fun state nd = State (SOME (nd, term));
    1.39 +        fun normal_state nd = (state nd, NONE);
    1.40 +        fun error_state nd exn = (state nd, SOME exn);
    1.41  
    1.42 -        val trans = if hist then History.apply_copy (copy_node int) else History.map;
    1.43 -        val (result, opt_exn) =
    1.44 -          (mk_state (transform_error (interruptible (trans (f int))) cont_node), NONE)
    1.45 -            handle exn => (mk_state cont_node, SOME exn);
    1.46 +        val (result, err) =
    1.47 +          cont_node
    1.48 +          |> ((fn nd => f int nd)
    1.49 +              |> (if hist then History.apply_copy (copy_node int) else History.map)
    1.50 +              |> debug_trans
    1.51 +              |> interruptible
    1.52 +              |> transform_error)
    1.53 +          |> normal_state
    1.54 +          handle exn => error_state cont_node exn;
    1.55        in
    1.56 -        if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback))
    1.57 -        else return (result, opt_exn)
    1.58 +        if is_stale result
    1.59 +        then return (error_state back_node (if_none err stale_theory))
    1.60 +        else return (result, err)
    1.61        end;
    1.62  
    1.63 -fun check_stale state =
    1.64 -  conditional (is_stale state) (fn () => warning "Stale theory encountered!");
    1.65 -
    1.66  end;
    1.67  
    1.68  
    1.69 @@ -478,8 +490,6 @@
    1.70  
    1.71  in
    1.72  
    1.73 -val debug = ref false;
    1.74 -
    1.75  fun exn_message exn = exn_msg (! debug) exn;
    1.76  
    1.77  fun print_exn NONE = ()
    1.78 @@ -503,8 +513,9 @@
    1.79      fun do_profiling f x = profile (! profiling) f x;
    1.80  
    1.81      val (result, opt_exn) =
    1.82 -      (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)
    1.83 -        ((if ! profiling > 0 then do_profiling else I) (apply_trans int trans)) state;
    1.84 +       state |> (apply_trans int trans
    1.85 +        |> (if ! profiling > 0 then do_profiling else I)
    1.86 +        |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
    1.87      val _ = conditional (int andalso not (! quiet) andalso
    1.88          exists (fn m => m mem_string print) ("" :: ! print_mode))
    1.89        (fn () => print_state false result);
    1.90 @@ -580,7 +591,7 @@
    1.91      NONE => false
    1.92    | SOME (state', exn_info) =>
    1.93        (global_state := (state', exn_info);
    1.94 -        check_stale state'; print_exn exn_info;
    1.95 +        print_exn exn_info;
    1.96          true));
    1.97  
    1.98  fun >>> [] = ()
    1.99 @@ -596,8 +607,6 @@
   1.100    | SOME NONE => ()
   1.101    | SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ());
   1.102  
   1.103 -
   1.104  fun loop src = ignore_interrupt raw_loop src;
   1.105  
   1.106 -
   1.107  end;