refined notion of empty toplevel, admits undo of 'end';
authorwenzelm
Sat Dec 30 12:33:28 2006 +0100 (2006-12-30)
changeset 219589dfd1ca4c0a0
parent 21957 4e44e74dc7e7
child 21959 b50182aff75f
refined notion of empty toplevel, admits undo of 'end';
added undo_exit, init_empty, init_state;
removed unused toplevel, reset;
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 30 12:33:27 2006 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Dec 30 12:33:28 2006 +0100
     1.3 @@ -15,7 +15,6 @@
     1.4    val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
     1.5    val presentation_context: node option -> xstring option -> Proof.context
     1.6    type state
     1.7 -  val toplevel: state
     1.8    val is_toplevel: state -> bool
     1.9    val is_theory: state -> bool
    1.10    val is_proof: state -> bool
    1.11 @@ -59,9 +58,10 @@
    1.12    val three_buffersN: string
    1.13    val print3: transition -> transition
    1.14    val no_timing: transition -> transition
    1.15 -  val reset: transition -> transition
    1.16    val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
    1.17 +  val init_empty: (state -> unit) -> transition -> transition
    1.18    val exit: transition -> transition
    1.19 +  val undo_exit: transition -> transition
    1.20    val kill: transition -> transition
    1.21    val history: (node History.T -> node History.T) -> transition -> transition
    1.22    val keep: (state -> unit) -> transition -> transition
    1.23 @@ -99,6 +99,7 @@
    1.24    val exn: unit -> (exn * string) option
    1.25    val >> : transition -> bool
    1.26    val >>> : transition list -> unit
    1.27 +  val init_state: unit -> unit
    1.28    type 'a isar
    1.29    val loop: 'a isar -> unit
    1.30  end;
    1.31 @@ -106,6 +107,7 @@
    1.32  structure Toplevel: TOPLEVEL =
    1.33  struct
    1.34  
    1.35 +
    1.36  (** toplevel state **)
    1.37  
    1.38  exception UNDEF;
    1.39 @@ -128,7 +130,7 @@
    1.40    | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o LocalTheory.reinit lthy o loc_exit;
    1.41  
    1.42  
    1.43 -(* datatype state *)
    1.44 +(* datatype node *)
    1.45  
    1.46  datatype node =
    1.47    Theory of generic_theory * Proof.context option | (*theory with presentation context*)
    1.48 @@ -150,22 +152,29 @@
    1.49        loc_init (SOME loc) (cases_node Context.theory_of Proof.theory_of node)
    1.50    | presentation_context NONE _ = raise UNDEF;
    1.51  
    1.52 -datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
    1.53 +
    1.54 +(* datatype state *)
    1.55 +
    1.56 +type state_info = node History.T * ((node -> unit) * (node -> unit));
    1.57  
    1.58 -val toplevel = State NONE;
    1.59 +datatype state =
    1.60 +  Toplevel of state_info option |  (*outer toplevel, leftover end state*)
    1.61 +  State of state_info;
    1.62  
    1.63 -fun is_toplevel (State NONE) = true
    1.64 +val toplevel = Toplevel NONE;
    1.65 +
    1.66 +fun is_toplevel (Toplevel _) = true
    1.67    | is_toplevel _ = false;
    1.68  
    1.69 -fun level (State NONE) = 0
    1.70 -  | level (State (SOME (node, _))) =
    1.71 +fun level (Toplevel _) = 0
    1.72 +  | level (State (node, _)) =
    1.73        (case History.current node of
    1.74          Theory _ => 0
    1.75        | Proof (prf, _) => Proof.level (ProofHistory.current prf)
    1.76        | SkipProof (h, _) => History.current h + 1);   (*different notion of proof depth!*)
    1.77  
    1.78 -fun str_of_state (State NONE) = "at top level"
    1.79 -  | str_of_state (State (SOME (node, _))) =
    1.80 +fun str_of_state (Toplevel _) = "at top level"
    1.81 +  | str_of_state (State (node, _)) =
    1.82        (case History.current node of
    1.83          Theory (Context.Theory _, _) => "in theory mode"
    1.84        | Theory (Context.Proof _, _) => "in local theory mode"
    1.85 @@ -175,8 +184,8 @@
    1.86  
    1.87  (* top node *)
    1.88  
    1.89 -fun node_history_of (State NONE) = raise UNDEF
    1.90 -  | node_history_of (State (SOME (node, _))) = node;
    1.91 +fun node_history_of (Toplevel _) = raise UNDEF
    1.92 +  | node_history_of (State (node, _)) = node;
    1.93  
    1.94  val node_of = History.current o node_history_of;
    1.95  
    1.96 @@ -199,7 +208,7 @@
    1.97  
    1.98  (* prompt state *)
    1.99  
   1.100 -fun prompt_state_default (State _) = Source.default_prompt;
   1.101 +fun prompt_state_default (_: state) = Source.default_prompt;
   1.102  
   1.103  val prompt_state_fn = ref prompt_state_default;
   1.104  fun prompt_state state = ! prompt_state_fn state;
   1.105 @@ -360,7 +369,7 @@
   1.106    let
   1.107      val cont_node = map_theory Theory.checkpoint node;
   1.108      val back_node = map_theory Theory.copy cont_node;
   1.109 -    fun state nd = State (SOME (nd, term));
   1.110 +    fun state nd = State (nd, term);
   1.111      fun normal_state nd = (state nd, NONE);
   1.112      fun error_state nd exn = (state nd, SOME exn);
   1.113  
   1.114 @@ -388,36 +397,39 @@
   1.115    Transaction.*)
   1.116  
   1.117  datatype trans =
   1.118 -  Reset |                                               (*empty toplevel*)
   1.119    Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
   1.120 -                                                        (*init node; with exit/kill operation*)
   1.121 -  Exit |                                                (*conclude node*)
   1.122 -  Kill |                                                (*abort node*)
   1.123 -  History of node History.T -> node History.T |         (*history operation (undo etc.)*)
   1.124 -  Keep of bool -> state -> unit |                       (*peek at state*)
   1.125 -  Transaction of bool * (bool -> node -> node);         (*node transaction*)
   1.126 +                                                    (*init node; with exit/kill operation*)
   1.127 +  InitEmpty of state -> unit |                      (*init empty toplevel*)
   1.128 +  Exit |                                            (*conclude node -- deferred until init*)
   1.129 +  UndoExit |                                        (*continue after conclusion*)
   1.130 +  Kill |                                            (*abort node*)
   1.131 +  History of node History.T -> node History.T |     (*history operation (undo etc.)*)
   1.132 +  Keep of bool -> state -> unit |                   (*peek at state*)
   1.133 +  Transaction of bool * (bool -> node -> node);     (*node transaction*)
   1.134  
   1.135  fun undo_limit int = if int then NONE else SOME 0;
   1.136  
   1.137 +fun apply_exit (Toplevel (SOME (node, (exit, _)))) = exit (History.current node)
   1.138 +  | apply_exit _ = ();
   1.139 +
   1.140  local
   1.141  
   1.142 -fun apply_tr _ Reset _ = toplevel
   1.143 -  | apply_tr int (Init (f, term)) (State NONE) =
   1.144 -      State (SOME (History.init (undo_limit int) (f int), term))
   1.145 -  | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF
   1.146 -  | apply_tr _ Exit (State NONE) = raise UNDEF
   1.147 -  | apply_tr _ Exit (State (SOME (node, (exit, _)))) =
   1.148 -      (exit (History.current node); State NONE)
   1.149 -  | apply_tr _ Kill (State NONE) = raise UNDEF
   1.150 -  | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
   1.151 -      (kill (History.current node); State NONE)
   1.152 -  | apply_tr _ (History _) (State NONE) = raise UNDEF
   1.153 -  | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
   1.154 -  | apply_tr int (Keep f) state =
   1.155 -      controlled_execution (fn x => tap (f int) x) state
   1.156 -  | apply_tr _ (Transaction _) (State NONE) = raise UNDEF
   1.157 -  | apply_tr int (Transaction (hist, f)) (State (SOME state)) =
   1.158 -      transaction hist (fn x => f int x) state;
   1.159 +fun keep_state int f = controlled_execution (fn x => tap (f int) x);
   1.160 +
   1.161 +fun apply_tr int (Init (f, term)) (state as Toplevel _) =
   1.162 +      let val node = f int
   1.163 +      in apply_exit state; State (History.init (undo_limit int) node, term) end
   1.164 +  | apply_tr int (InitEmpty f) state =
   1.165 +      (keep_state int (K f) state; apply_exit state; toplevel)
   1.166 +  | apply_tr _ Exit (State state) = Toplevel (SOME state)
   1.167 +  | apply_tr _ UndoExit (Toplevel (SOME state)) = State state
   1.168 +  | apply_tr _ Kill (State (node, (_, kill))) =
   1.169 +      (kill (History.current node); toplevel)
   1.170 +  | apply_tr _ (History f) (State (node, term)) = State (f node, term)
   1.171 +  | apply_tr int (Keep f) state = keep_state int f state
   1.172 +  | apply_tr int (Transaction (hist, f)) (State state) =
   1.173 +      transaction hist (fn x => f int x) state
   1.174 +  | apply_tr _ _ _ = raise UNDEF;
   1.175  
   1.176  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   1.177    | apply_union int (tr :: trs) state =
   1.178 @@ -501,9 +513,10 @@
   1.179  
   1.180  (* basic transitions *)
   1.181  
   1.182 -val reset = add_trans Reset;
   1.183  fun init f exit kill = add_trans (Init (f, (exit, kill)));
   1.184 +val init_empty = add_trans o InitEmpty;
   1.185  val exit = add_trans Exit;
   1.186 +val undo_exit = add_trans UndoExit;
   1.187  val kill = add_trans Kill;
   1.188  val history = add_trans o History;
   1.189  val keep' = add_trans o Keep;
   1.190 @@ -694,8 +707,8 @@
   1.191  in
   1.192  
   1.193  fun present_excursion trs res =
   1.194 -  (case excur trs (State NONE, res) of
   1.195 -    (State NONE, res') => res'
   1.196 +  (case excur trs (toplevel, res) of
   1.197 +    (state as Toplevel _, res') => (apply_exit state; res')
   1.198    | _ => error "Unfinished development at end of input")
   1.199    handle exn => error (exn_message exn);
   1.200  
   1.201 @@ -716,15 +729,6 @@
   1.202  fun exn () = snd (! global_state);
   1.203  
   1.204  
   1.205 -(* the Isar source of transitions *)
   1.206 -
   1.207 -type 'a isar =
   1.208 -  (transition, (transition option,
   1.209 -    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
   1.210 -      Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
   1.211 -          Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
   1.212 -
   1.213 -
   1.214  (* apply transformers to global state *)
   1.215  
   1.216  nonfix >> >>>;
   1.217 @@ -740,6 +744,17 @@
   1.218  fun >>> [] = ()
   1.219    | >>> (tr :: trs) = if >> tr then >>> trs else ();
   1.220  
   1.221 +fun init_state () = (>> (init_empty (K ()) empty); ());
   1.222 +
   1.223 +
   1.224 +(* the Isar source of transitions *)
   1.225 +
   1.226 +type 'a isar =
   1.227 +  (transition, (transition option,
   1.228 +    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
   1.229 +      Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
   1.230 +          Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
   1.231 +
   1.232  (*Spurious interrupts ahead!  Race condition?*)
   1.233  fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
   1.234