equal
deleted
inserted
replaced
66 fun update_calculation calc state = |
66 fun update_calculation calc state = |
67 let |
67 let |
68 fun report def serial pos = |
68 fun report def serial pos = |
69 Context_Position.report (Proof.context_of state) |
69 Context_Position.report (Proof.context_of state) |
70 (Position.thread_data ()) |
70 (Position.thread_data ()) |
71 (Markup.entity calculationN "" |
71 (Position.make_entity_markup def serial calculationN ("", pos)); |
72 |> Markup.properties (Position.entity_properties_of def serial pos)); |
|
73 val calculation = |
72 val calculation = |
74 (case calc of |
73 (case calc of |
75 NONE => NONE |
74 NONE => NONE |
76 | SOME result => |
75 | SOME result => |
77 (case check_calculation state of |
76 (case check_calculation state of |