20 and the block structure of proofs, support for unlimited undo, |
20 and the block structure of proofs, support for unlimited undo, |
21 facilities for tracing, debugging, timing, profiling etc. |
21 facilities for tracing, debugging, timing, profiling etc. |
22 |
22 |
23 \medskip The toplevel maintains an implicit state, which is |
23 \medskip The toplevel maintains an implicit state, which is |
24 transformed by a sequence of transitions -- either interactively or |
24 transformed by a sequence of transitions -- either interactively or |
25 in batch-mode. In interactive mode, Isar state transitions are |
25 in batch-mode. |
26 encapsulated as safe transactions, such that both failure and undo |
|
27 are handled conveniently without destroying the underlying draft |
|
28 theory (cf.~\secref{sec:context-theory}). In batch mode, |
|
29 transitions operate in a linear (destructive) fashion, such that |
|
30 error conditions abort the present attempt to construct a theory or |
|
31 proof altogether. |
|
32 |
26 |
33 The toplevel state is a disjoint sum of empty @{text toplevel}, or |
27 The toplevel state is a disjoint sum of empty @{text toplevel}, or |
34 @{text theory}, or @{text proof}. On entering the main Isar loop we |
28 @{text theory}, or @{text proof}. On entering the main Isar loop we |
35 start with an empty toplevel. A theory is commenced by giving a |
29 start with an empty toplevel. A theory is commenced by giving a |
36 @{text \<THEORY>} header; within a theory we may issue theory |
30 @{text \<THEORY>} header; within a theory we may issue theory |