equal
deleted
inserted
replaced
746 file_pos = Position.file node_name, |
746 file_pos = Position.file node_name, |
747 adjust_pos = Position.adjust_offsets adjust, |
747 adjust_pos = Position.adjust_offsets adjust, |
748 segments = segments}; |
748 segments = segments}; |
749 in |
749 in |
750 fn _ => |
750 fn _ => |
751 Exn.release |
751 let |
752 (Exn.capture (Thy_Info.apply_presentation presentation_context) thy |
752 val _ = Output.status [Markup.markup_only Markup.consolidating]; |
753 before commit_consolidated node) |
753 val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; |
|
754 val _ = commit_consolidated node; |
|
755 in Exn.release res end |
754 end |
756 end |
755 else fn _ => commit_consolidated node; |
757 else fn _ => commit_consolidated node; |
756 |
758 |
757 val result_entry = |
759 val result_entry = |
758 (case lookup_entry node result_id of |
760 (case lookup_entry node result_id of |