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