equal
deleted
inserted
replaced
1029 (* skip proofs *) |
1029 (* skip proofs *) |
1030 |
1030 |
1031 local |
1031 local |
1032 |
1032 |
1033 fun skipped_proof state = |
1033 fun skipped_proof state = |
1034 Context_Position.report_text (context_of state) (Position.thread_data ()) |
1034 Context_Position.if_visible (context_of state) Output.report |
1035 Markup.bad "Skipped proof"; |
1035 (Markup.markup Markup.bad "Skipped proof"); |
1036 |
1036 |
1037 in |
1037 in |
1038 |
1038 |
1039 fun local_skip_proof int state = |
1039 fun local_skip_proof int state = |
1040 local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before |
1040 local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before |