src/Pure/Isar/toplevel.ML
changeset 18685 725660906cb3
parent 18664 ad7ae7870427
child 18718 d01837224eaf
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jan 14 17:14:17 2006 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jan 14 17:14:18 2006 +0100
     1.3 @@ -94,6 +94,7 @@
     1.4    val command: transition -> state -> state
     1.5    val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
     1.6    val excursion: transition list -> unit
     1.7 +  val program: (unit -> 'a) -> 'a
     1.8    val set_state: state -> unit
     1.9    val get_state: unit -> state
    1.10    val exn: unit -> (exn * string) option
    1.11 @@ -241,6 +242,12 @@
    1.12  exception EXCURSION_FAIL of exn * string;
    1.13  exception FAILURE of state * exn;
    1.14  
    1.15 +fun debugging f x =
    1.16 +  if ! debug then
    1.17 +    setmp Library.do_transform_failure false
    1.18 +      exception_trace (fn () => f x)
    1.19 +  else f x;
    1.20 +
    1.21  
    1.22  (* node transactions and recovery from stale theories *)
    1.23  
    1.24 @@ -250,7 +257,7 @@
    1.25  
    1.26  fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
    1.27  
    1.28 -val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
    1.29 +val stale_theory = ERROR "Stale theory encountered after succesful execution!";
    1.30  
    1.31  fun checkpoint_node (Theory (thy, ctxt)) = Theory (Theory.checkpoint thy, ctxt)
    1.32    | checkpoint_node node = node;
    1.33 @@ -261,12 +268,6 @@
    1.34  fun return (result, NONE) = result
    1.35    | return (result, SOME exn) = raise FAILURE (result, exn);
    1.36  
    1.37 -fun debug_trans f x =
    1.38 -  if ! debug then
    1.39 -    setmp Output.transform_exceptions false
    1.40 -      exception_trace (fn () => f x)
    1.41 -  else f x;
    1.42 -
    1.43  fun interruptible f x =
    1.44    let val y = ref x
    1.45    in raise_interrupt (fn () => y := f x) (); ! y end;
    1.46 @@ -286,9 +287,9 @@
    1.47            cont_node
    1.48            |> (f
    1.49                |> (if hist then History.apply_copy copy_node else History.map)
    1.50 -              |> debug_trans
    1.51 +              |> debugging
    1.52                |> interruptible
    1.53 -              |> transform_error)
    1.54 +              |> setmp Output.do_toplevel_errors false)
    1.55            |> normal_state
    1.56            handle exn => error_state cont_node exn;
    1.57        in
    1.58 @@ -345,7 +346,7 @@
    1.59  
    1.60  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
    1.61    | apply_union int (tr :: trs) state =
    1.62 -      transform_error (apply_tr int tr) state
    1.63 +      apply_tr int tr state
    1.64          handle UNDEF => apply_union int trs state
    1.65            | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
    1.66            | exn as FAILURE _ => raise exn
    1.67 @@ -391,7 +392,7 @@
    1.68  fun at_command tr = command_msg "At " tr ^ ".";
    1.69  
    1.70  fun type_error tr state =
    1.71 -  ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
    1.72 +  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
    1.73  
    1.74  
    1.75  (* modify transitions *)
    1.76 @@ -519,15 +520,12 @@
    1.77  fun exn_msg _ TERMINATE = "Exit."
    1.78    | exn_msg _ RESTART = "Restart."
    1.79    | exn_msg _ Interrupt = "Interrupt."
    1.80 -  | exn_msg _ ERROR = "ERROR."
    1.81 -  | exn_msg _ (ERROR_MESSAGE msg) = msg
    1.82 +  | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
    1.83 +  | exn_msg _ (ERROR msg) = msg
    1.84    | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
    1.85    | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
    1.86    | exn_msg false (THEORY (msg, _)) = msg
    1.87    | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
    1.88 -  | exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg
    1.89 -  | exn_msg _ (Proof.STATE (msg, _)) = msg
    1.90 -  | exn_msg _ (ProofHistory.FAIL msg) = msg
    1.91    | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
    1.92        fail_msg detailed "simproc" ((name, Position.none), exn)
    1.93    | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
    1.94 @@ -558,7 +556,7 @@
    1.95  fun exn_message exn = exn_msg (! debug) exn;
    1.96  
    1.97  fun print_exn NONE = ()
    1.98 -  | print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
    1.99 +  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
   1.100  
   1.101  end;
   1.102  
   1.103 @@ -572,7 +570,7 @@
   1.104      val _ = conditional (not int andalso int_only) (fn () =>
   1.105        warning (command_msg "Interactive-only " tr));
   1.106  
   1.107 -    fun do_timing f x = (info (command_msg "" tr); timeap f x);
   1.108 +    fun do_timing f x = (Output.info (command_msg "" tr); timeap f x);
   1.109      fun do_profiling f x = profile (! profiling) f x;
   1.110  
   1.111      val (result, opt_exn) =
   1.112 @@ -611,7 +609,7 @@
   1.113    | excur ((tr, pr) :: trs) (st, res) =
   1.114        (case apply (! interact) tr st of
   1.115          SOME (st', NONE) =>
   1.116 -          excur trs (st', transform_error (fn () => pr st st' res) () handle exn =>
   1.117 +          excur trs (st', pr st st' res handle exn =>
   1.118              raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
   1.119        | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
   1.120        | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   1.121 @@ -623,7 +621,7 @@
   1.122  fun present_excursion trs res =
   1.123    (case excur trs (State NONE, res) of
   1.124      (State NONE, res') => res'
   1.125 -  | _ => raise ERROR_MESSAGE "Unfinished development at end of input")
   1.126 +  | _ => error "Unfinished development at end of input")
   1.127    handle exn => error (exn_message exn);
   1.128  
   1.129  fun excursion trs = present_excursion (map (rpair no_pr) trs) ();
   1.130 @@ -631,6 +629,14 @@
   1.131  end;
   1.132  
   1.133  
   1.134 +(* program: independent of state *)
   1.135 +
   1.136 +fun program f =
   1.137 +  ((fn () => debugging f () handle exn => error (exn_message exn))
   1.138 +    |> setmp Output.do_toplevel_errors true
   1.139 +    |> Output.toplevel_errors) ();
   1.140 +
   1.141 +
   1.142  
   1.143  (** interactive transformations **)
   1.144