equal
deleted
inserted
replaced
11 type generic_theory |
11 type generic_theory |
12 type node |
12 type node |
13 val theory_node: node -> generic_theory option |
13 val theory_node: node -> generic_theory option |
14 val proof_node: node -> ProofNode.T option |
14 val proof_node: node -> ProofNode.T option |
15 val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a |
15 val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a |
|
16 val context_node: node -> Proof.context |
16 val presentation_context: node option -> xstring option -> Proof.context |
17 val presentation_context: node option -> xstring option -> Proof.context |
17 type state |
18 type state |
18 val toplevel: state |
19 val toplevel: state |
19 val is_toplevel: state -> bool |
20 val is_toplevel: state -> bool |
20 val is_theory: state -> bool |
21 val is_theory: state -> bool |
138 |
139 |
139 fun cases_node f _ (Theory (gthy, _)) = f gthy |
140 fun cases_node f _ (Theory (gthy, _)) = f gthy |
140 | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf) |
141 | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf) |
141 | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; |
142 | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; |
142 |
143 |
|
144 val context_node = cases_node Context.proof_of Proof.context_of; |
|
145 |
143 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt |
146 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt |
144 | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node |
147 | presentation_context (SOME node) NONE = context_node node |
145 | presentation_context (SOME node) (SOME loc) = |
148 | presentation_context (SOME node) (SOME loc) = |
146 loc_init loc (cases_node Context.theory_of Proof.theory_of node) |
149 loc_init loc (cases_node Context.theory_of Proof.theory_of node) |
147 | presentation_context NONE _ = raise UNDEF; |
150 | presentation_context NONE _ = raise UNDEF; |
148 |
151 |
149 fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) |
152 fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) |