equal
deleted
inserted
replaced
5 The Isabelle/Isar toplevel. |
5 The Isabelle/Isar toplevel. |
6 *) |
6 *) |
7 |
7 |
8 signature TOPLEVEL = |
8 signature TOPLEVEL = |
9 sig |
9 sig |
10 datatype node = Theory of theory | Proof of ProofHistory.T |
10 datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory |
11 | SkipProof of int History.T * theory |
|
12 type state |
11 type state |
13 val toplevel: state |
12 val toplevel: state |
14 val is_toplevel: state -> bool |
13 val is_toplevel: state -> bool |
15 val prompt_state_default: state -> string |
14 val prompt_state_default: state -> string |
16 val prompt_state_fn: (state -> string) ref |
15 val prompt_state_fn: (state -> string) ref |
226 if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback)) |
225 if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback)) |
227 else return (result, opt_exn) |
226 else return (result, opt_exn) |
228 end; |
227 end; |
229 |
228 |
230 fun check_stale state = |
229 fun check_stale state = |
231 if not (is_stale state) then () |
230 conditional (is_stale state) (fn () => warning "Stale theory encountered!"); |
232 else warning "Stale theory encountered!"; |
|
233 |
231 |
234 end; |
232 end; |
235 |
233 |
236 |
234 |
237 (* primitive transitions *) |
235 (* primitive transitions *) |