# HG changeset patch # User wenzelm # Date 1167478408 -3600 # Node ID 9dfd1ca4c0a070860dc17e95816e780e28628c6a # Parent 4e44e74dc7e751a4a942014048b0d52206366cee refined notion of empty toplevel, admits undo of 'end'; added undo_exit, init_empty, init_state; removed unused toplevel, reset; tuned; diff -r 4e44e74dc7e7 -r 9dfd1ca4c0a0 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Dec 30 12:33:27 2006 +0100 +++ b/src/Pure/Isar/toplevel.ML Sat Dec 30 12:33:28 2006 +0100 @@ -15,7 +15,6 @@ val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a val presentation_context: node option -> xstring option -> Proof.context type state - val toplevel: state val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool @@ -59,9 +58,10 @@ val three_buffersN: string val print3: transition -> transition val no_timing: transition -> transition - val reset: transition -> transition val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition + val init_empty: (state -> unit) -> transition -> transition val exit: transition -> transition + val undo_exit: transition -> transition val kill: transition -> transition val history: (node History.T -> node History.T) -> transition -> transition val keep: (state -> unit) -> transition -> transition @@ -99,6 +99,7 @@ val exn: unit -> (exn * string) option val >> : transition -> bool val >>> : transition list -> unit + val init_state: unit -> unit type 'a isar val loop: 'a isar -> unit end; @@ -106,6 +107,7 @@ structure Toplevel: TOPLEVEL = struct + (** toplevel state **) exception UNDEF; @@ -128,7 +130,7 @@ | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o LocalTheory.reinit lthy o loc_exit; -(* datatype state *) +(* datatype node *) datatype node = Theory of generic_theory * Proof.context option | (*theory with presentation context*) @@ -150,22 +152,29 @@ loc_init (SOME loc) (cases_node Context.theory_of Proof.theory_of node) | presentation_context NONE _ = raise UNDEF; -datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option; + +(* datatype state *) + +type state_info = node History.T * ((node -> unit) * (node -> unit)); -val toplevel = State NONE; +datatype state = + Toplevel of state_info option | (*outer toplevel, leftover end state*) + State of state_info; -fun is_toplevel (State NONE) = true +val toplevel = Toplevel NONE; + +fun is_toplevel (Toplevel _) = true | is_toplevel _ = false; -fun level (State NONE) = 0 - | level (State (SOME (node, _))) = +fun level (Toplevel _) = 0 + | level (State (node, _)) = (case History.current node of Theory _ => 0 | Proof (prf, _) => Proof.level (ProofHistory.current prf) | SkipProof (h, _) => History.current h + 1); (*different notion of proof depth!*) -fun str_of_state (State NONE) = "at top level" - | str_of_state (State (SOME (node, _))) = +fun str_of_state (Toplevel _) = "at top level" + | str_of_state (State (node, _)) = (case History.current node of Theory (Context.Theory _, _) => "in theory mode" | Theory (Context.Proof _, _) => "in local theory mode" @@ -175,8 +184,8 @@ (* top node *) -fun node_history_of (State NONE) = raise UNDEF - | node_history_of (State (SOME (node, _))) = node; +fun node_history_of (Toplevel _) = raise UNDEF + | node_history_of (State (node, _)) = node; val node_of = History.current o node_history_of; @@ -199,7 +208,7 @@ (* prompt state *) -fun prompt_state_default (State _) = Source.default_prompt; +fun prompt_state_default (_: state) = Source.default_prompt; val prompt_state_fn = ref prompt_state_default; fun prompt_state state = ! prompt_state_fn state; @@ -360,7 +369,7 @@ let val cont_node = map_theory Theory.checkpoint node; val back_node = map_theory Theory.copy cont_node; - fun state nd = State (SOME (nd, term)); + fun state nd = State (nd, term); fun normal_state nd = (state nd, NONE); fun error_state nd exn = (state nd, SOME exn); @@ -388,36 +397,39 @@ Transaction.*) datatype trans = - Reset | (*empty toplevel*) Init of (bool -> node) * ((node -> unit) * (node -> unit)) | - (*init node; with exit/kill operation*) - Exit | (*conclude node*) - Kill | (*abort node*) - History of node History.T -> node History.T | (*history operation (undo etc.)*) - Keep of bool -> state -> unit | (*peek at state*) - Transaction of bool * (bool -> node -> node); (*node transaction*) + (*init node; with exit/kill operation*) + InitEmpty of state -> unit | (*init empty toplevel*) + Exit | (*conclude node -- deferred until init*) + UndoExit | (*continue after conclusion*) + Kill | (*abort node*) + History of node History.T -> node History.T | (*history operation (undo etc.)*) + Keep of bool -> state -> unit | (*peek at state*) + Transaction of bool * (bool -> node -> node); (*node transaction*) fun undo_limit int = if int then NONE else SOME 0; +fun apply_exit (Toplevel (SOME (node, (exit, _)))) = exit (History.current node) + | apply_exit _ = (); + local -fun apply_tr _ Reset _ = toplevel - | apply_tr int (Init (f, term)) (State NONE) = - State (SOME (History.init (undo_limit int) (f int), term)) - | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF - | apply_tr _ Exit (State NONE) = raise UNDEF - | apply_tr _ Exit (State (SOME (node, (exit, _)))) = - (exit (History.current node); State NONE) - | apply_tr _ Kill (State NONE) = raise UNDEF - | apply_tr _ Kill (State (SOME (node, (_, kill)))) = - (kill (History.current node); State NONE) - | apply_tr _ (History _) (State NONE) = raise UNDEF - | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) - | apply_tr int (Keep f) state = - controlled_execution (fn x => tap (f int) x) state - | apply_tr _ (Transaction _) (State NONE) = raise UNDEF - | apply_tr int (Transaction (hist, f)) (State (SOME state)) = - transaction hist (fn x => f int x) state; +fun keep_state int f = controlled_execution (fn x => tap (f int) x); + +fun apply_tr int (Init (f, term)) (state as Toplevel _) = + let val node = f int + in apply_exit state; State (History.init (undo_limit int) node, term) end + | apply_tr int (InitEmpty f) state = + (keep_state int (K f) state; apply_exit state; toplevel) + | apply_tr _ Exit (State state) = Toplevel (SOME state) + | apply_tr _ UndoExit (Toplevel (SOME state)) = State state + | apply_tr _ Kill (State (node, (_, kill))) = + (kill (History.current node); toplevel) + | apply_tr _ (History f) (State (node, term)) = State (f node, term) + | apply_tr int (Keep f) state = keep_state int f state + | apply_tr int (Transaction (hist, f)) (State state) = + transaction hist (fn x => f int x) state + | apply_tr _ _ _ = raise UNDEF; fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = @@ -501,9 +513,10 @@ (* basic transitions *) -val reset = add_trans Reset; fun init f exit kill = add_trans (Init (f, (exit, kill))); +val init_empty = add_trans o InitEmpty; val exit = add_trans Exit; +val undo_exit = add_trans UndoExit; val kill = add_trans Kill; val history = add_trans o History; val keep' = add_trans o Keep; @@ -694,8 +707,8 @@ in fun present_excursion trs res = - (case excur trs (State NONE, res) of - (State NONE, res') => res' + (case excur trs (toplevel, res) of + (state as Toplevel _, res') => (apply_exit state; res') | _ => error "Unfinished development at end of input") handle exn => error (exn_message exn); @@ -716,15 +729,6 @@ fun exn () = snd (! global_state); -(* the Isar source of transitions *) - -type 'a isar = - (transition, (transition option, - (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, - Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) - Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; - - (* apply transformers to global state *) nonfix >> >>>; @@ -740,6 +744,17 @@ fun >>> [] = () | >>> (tr :: trs) = if >> tr then >>> trs else (); +fun init_state () = (>> (init_empty (K ()) empty); ()); + + +(* the Isar source of transitions *) + +type 'a isar = + (transition, (transition option, + (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, + Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) + Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; + (*Spurious interrupts ahead! Race condition?*) fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;