# HG changeset patch # User wenzelm # Date 1222810300 -7200 # Node ID 32bb6b4eb39094798188aed026456d299cc33e25 # Parent 0790f66a931a0e2142503d7407c0a9c33c4fc322 unit_source: explicit treatment of 'oops' proofs; diff -r 0790f66a931a -r 32bb6b4eb390 src/Pure/Thy/thy_edit.ML --- a/src/Pure/Thy/thy_edit.ML Tue Sep 30 23:31:38 2008 +0200 +++ b/src/Pure/Thy/thy_edit.ML Tue Sep 30 23:31:40 2008 +0200 @@ -24,7 +24,7 @@ val present_span: span -> output val report_span: span -> unit val unit_source: (span, 'a) Source.source -> - (span * span list, (span, 'a) Source.source) Source.source + (span * span list * bool, (span, 'a) Source.source) Source.source end; structure ThyEdit: THY_EDIT = @@ -179,9 +179,11 @@ command_with K.is_proof_goal >> pair (d + 1) || (if d <= 1 then Scan.fail else command_with K.is_qed >> pair (d - 1)) || command_with K.is_qed_global >> pair 0 || - Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d))); + Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state); -val unit = command_with K.is_theory_goal -- proof || Scan.one not_eof >> rpair []; +val unit = + command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d <> 0)) || + Scan.one not_eof >> (fn a => (a, [], true)); in