# HG changeset patch
# User wenzelm
# Date 1222804973 -7200
# Node ID 56f0951f4d2635ccea71454e1a209d489039fabf
# Parent  b3dab95f098ffbb9040ec71a59d9ac14750f41d2
added unit_source: commands with proof;

diff -r b3dab95f098f -r 56f0951f4d26 src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Tue Sep 30 22:02:51 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Tue Sep 30 22:02:53 2008 +0200
@@ -23,11 +23,14 @@
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   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
 end;
 
 structure ThyEdit: THY_EDIT =
 struct
 
+structure K = OuterKeyword;
 structure T = OuterLex;
 structure P = OuterParse;
 
@@ -148,4 +151,42 @@
 
 end;
 
+
+
+(** units: commands with proof **)
+
+(* scanning spans *)
+
+val eof = Span (Command "", []);
+
+fun is_eof (Span (Command "", _)) = true
+  | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+val stopper = Scan.stopper (K eof) is_eof;
+
+
+(* unit_source *)
+
+local
+
+fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false);
+
+val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
+  if d = 0 then Scan.fail
+  else
+    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)));
+
+val unit = command_with K.is_theory_goal -- proof || Scan.one not_eof >> rpair [];
+
+in
+
+fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src;
+
 end;
+
+end;