cleaned comments;
authorwenzelm
Mon May 17 21:34:45 1999 +0200 (1999-05-17 ago)
changeset 6664f679ddd1ddd8
parent 6663 3f87294c8704
child 6665 bf421d724db7
cleaned comments;
node_cases renamed to node_case;
more robust rollback of transactions via backup;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon May 17 21:33:22 1999 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon May 17 21:34:45 1999 +0200
     1.3 @@ -3,16 +3,6 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  The Isabelle/Isar toplevel.
     1.7 -
     1.8 -TODO:
     1.9 -  - cleanup this file:
    1.10 -      . more internal locality;
    1.11 -      . clearer structure of control flow (exceptions, interrupts);
    1.12 -      . clear division with outer_syntax.ML (!?);
    1.13 -  - improve transactions; only in interactive mode!
    1.14 -  - init / exit proof;
    1.15 -  - display stack size in prompt (prompt: state -> string (hook));
    1.16 -  - excursion: more robust checking of begin / end theory match (including correct name);
    1.17  *)
    1.18  
    1.19  signature TOPLEVEL =
    1.20 @@ -25,7 +15,7 @@
    1.21    val print_state_fn: (state -> unit) ref
    1.22    val print_state: state -> unit
    1.23    val node_of: state -> node
    1.24 -  val node_cases: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    1.25 +  val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    1.26    val theory_of: state -> theory
    1.27    val sign_of: state -> Sign.sg
    1.28    val proof_of: state -> Proof.state
    1.29 @@ -44,10 +34,6 @@
    1.30    val exit: transition -> transition
    1.31    val imperative: (unit -> unit) -> transition -> transition
    1.32    val init_theory: (unit -> theory) -> (theory -> unit) -> transition -> transition
    1.33 -(* FIXME
    1.34 -  val init_proof: (theory -> ProofHistory.T) -> transition -> transition
    1.35 -  val exit_proof: (ProofHistory.T -> unit) -> transition -> transition
    1.36 -*)
    1.37    val theory: (theory -> theory) -> transition -> transition
    1.38    val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.39    val theory_to_proof: (theory -> ProofHistory.T) -> transition -> transition
    1.40 @@ -121,14 +107,21 @@
    1.41  fun node_of (State []) = raise UNDEF
    1.42    | node_of (State ((node, _) :: _)) = node;
    1.43  
    1.44 -fun node_cases f g state =
    1.45 +fun node_case f g state =
    1.46    (case node_of state of
    1.47      Theory thy => f thy
    1.48    | Proof prf => g (ProofHistory.current prf));
    1.49  
    1.50 -val theory_of = node_cases I Proof.theory_of;
    1.51 +val theory_of = node_case I Proof.theory_of;
    1.52  val sign_of = Theory.sign_of o theory_of;
    1.53 -val proof_of = node_cases (fn _ => raise UNDEF) I;
    1.54 +val proof_of = node_case (fn _ => raise UNDEF) I;
    1.55 +
    1.56 +fun is_stale state =
    1.57 +  Sign.is_stale (node_case Theory.sign_of Proof.sign_of state) handle UNDEF => false;
    1.58 +
    1.59 +fun backup (State ((Theory thy, exit) :: nodes)) =
    1.60 +      State ((Theory (PureThy.backup thy), exit) :: nodes)
    1.61 +  | backup state = state;
    1.62  
    1.63  
    1.64  
    1.65 @@ -222,8 +215,7 @@
    1.66  fun init_theory f g =
    1.67    init (fn _ => Theory (f ())) (fn Theory thy => g thy | _ => raise UNDEF);
    1.68  
    1.69 -fun theory f = map_current
    1.70 -  (fn Theory thy => Theory (PureThy.transaction f thy) | _ => raise UNDEF);
    1.71 +fun theory f = map_current (fn Theory thy => Theory (f thy) | _ => raise UNDEF);
    1.72  fun proof f = map_current (fn Proof prf => Proof (f prf) | _ => raise UNDEF);
    1.73  
    1.74  fun theory_to_proof f = map_current (fn Theory thy => Proof (f thy) | _ => raise UNDEF);
    1.75 @@ -291,17 +283,15 @@
    1.76  (* the dreaded stale signatures *)
    1.77  
    1.78  fun check_stale state =
    1.79 -  (case try theory_of state of
    1.80 -    None => ()
    1.81 -  | Some thy =>
    1.82 -      if Sign.is_stale (Theory.sign_of thy) then
    1.83 -        warning "Stale signature encountered!  Should redo current theory from start."
    1.84 -      else ());
    1.85 +  if not (is_stale state) then ()
    1.86 +  else warning "Stale signature encountered!  Should redo current theory from start.";
    1.87  
    1.88  
    1.89  (* apply transitions *)
    1.90  
    1.91 -fun app int (tr as Transition {trans, int_only, print, ...}) state =
    1.92 +local
    1.93 +
    1.94 +fun ap int (tr as Transition {trans, int_only, print, ...}) state =
    1.95    let
    1.96      val _ =
    1.97        if int orelse not int_only then ()
    1.98 @@ -313,26 +303,36 @@
    1.99      val _ = if int andalso print then print_state state' else ();
   1.100    in state' end;
   1.101  
   1.102 -fun rollback tr copy_thy (State ((Theory _, g) :: nodes)) =
   1.103 -      (warning (command_msg "Rollback after " tr); State ((Theory copy_thy, g) :: nodes))
   1.104 -  | rollback tr _ state =
   1.105 -      (warning (command_msg "Ignoring rollback theory copy from " tr); state);
   1.106 +fun app int tr state =
   1.107 +  let
   1.108 +    val back_state = backup state;
   1.109 +    fun rollback st =
   1.110 +      if not (is_stale st) then st
   1.111 +      else (warning (command_msg "Rollback after " tr); back_state);
   1.112 +  in
   1.113 +    (rollback (transform_interrupt_state (transform_error (ap int tr)) state), None)
   1.114 +      handle exn => (rollback state, Some exn)
   1.115 +  end;
   1.116 +
   1.117 +in
   1.118  
   1.119  fun apply int tr state =
   1.120 -  Some (transform_interrupt_state (transform_error (app int tr)) state, None)
   1.121 -    handle
   1.122 -      TERMINATE => None
   1.123 -    | RESTART => Some (toplevel, None)
   1.124 -    | FAIL (exn_info as (BREAK break_state, _)) =>
   1.125 -        Some (append_states break_state state, Some exn_info)
   1.126 -    | FAIL exn_info => Some (state, Some exn_info)
   1.127 -    | PureThy.ROLLBACK (copy_thy, opt_exn) =>
   1.128 -        Some (rollback tr copy_thy state, apsome (fn exn => (exn, at_command tr)) opt_exn)
   1.129 -    | exn => Some (state, Some (exn, at_command tr));
   1.130 +  (case app int tr state of
   1.131 +    (state', None) => Some (state', None)
   1.132 +  | (_, Some TERMINATE) => None
   1.133 +  | (_, Some RESTART) => Some (toplevel, None)
   1.134 +  | (state', Some (FAIL (exn_info as (BREAK break_state, _)))) =>
   1.135 +      Some (append_states break_state state', Some exn_info)
   1.136 +  | (state', Some (FAIL exn_info)) => Some (state', Some exn_info)
   1.137 +  | (state', Some exn) => Some (state', Some (exn, at_command tr)));
   1.138 +
   1.139 +end;
   1.140  
   1.141  
   1.142  (* excursion: toplevel -- apply transformers -- toplevel *)
   1.143  
   1.144 +local
   1.145 +
   1.146  fun excur [] x = x
   1.147    | excur (tr :: trs) x =
   1.148        (case apply false tr x of
   1.149 @@ -340,11 +340,15 @@
   1.150        | Some (x', Some exn_info) => raise FAIL exn_info
   1.151        | None => raise FAIL (TERMINATE, at_command tr));
   1.152  
   1.153 +in
   1.154 +
   1.155  fun excursion trs =
   1.156    (case excur trs (State []) of
   1.157      State [] => ()
   1.158    | _ => raise ERROR_MESSAGE "Open block(s) pending at end of input");
   1.159  
   1.160 +end;
   1.161 +
   1.162  
   1.163  
   1.164  (** interactive transformations **)