--- 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