159 | is_toplevel _ = false; |
159 | is_toplevel _ = false; |
160 |
160 |
161 fun level (State NONE) = 0 |
161 fun level (State NONE) = 0 |
162 | level (State (SOME (node, _))) = |
162 | level (State (SOME (node, _))) = |
163 (case History.current node of |
163 (case History.current node of |
164 Theory (Context.Theory _, _) => 0 |
164 Theory _ => 0 |
165 | Theory (Context.Proof _, _) => 1 |
165 | Proof (prf, _) => Proof.level (ProofHistory.current prf) |
166 | Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1 |
166 | SkipProof (h, _) => History.current h + 1); (*different notion of proof depth!*) |
167 | SkipProof (h, _) => History.current h + 2); (*different notion of proof depth!*) |
|
168 |
167 |
169 fun str_of_state (State NONE) = "at top level" |
168 fun str_of_state (State NONE) = "at top level" |
170 | str_of_state (State (SOME (node, _))) = |
169 | str_of_state (State (SOME (node, _))) = |
171 (case History.current node of |
170 (case History.current node of |
172 Theory (Context.Theory _, _) => "in theory mode" |
171 Theory (Context.Theory _, _) => "in theory mode" |