equal
deleted
inserted
replaced
120 Context_Position.report (Proof.context_of state) (Position.thread_data ()) Markup.improper |
120 Context_Position.report (Proof.context_of state) (Position.thread_data ()) Markup.improper |
121 else ()); |
121 else ()); |
122 |
122 |
123 fun maintain_calculation int final calc state = |
123 fun maintain_calculation int final calc state = |
124 let |
124 let |
125 val state' = put_calculation (SOME calc) state; |
125 val state' = state |
|
126 |> put_calculation (SOME calc) |
|
127 |> Proof.improper_reset_facts; |
126 val ctxt' = Proof.context_of state'; |
128 val ctxt' = Proof.context_of state'; |
127 val _ = |
129 val _ = |
128 if int then |
130 if int then |
129 Proof_Context.pretty_fact ctxt' |
131 Proof_Context.pretty_fact ctxt' |
130 (Proof_Context.full_name ctxt' (Binding.name calculationN), calc) |
132 (Proof_Context.full_name ctxt' (Binding.name calculationN), calc) |