# 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