support nested Thy_Syntax.element;
more explicit Keyword.is_proof_body;
tuned;

--- a/src/Pure/Isar/keyword.ML	Tue Feb 19 21:44:37 2013 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Feb 20 00:00:42 2013 +0100
@@ -63,6 +63,7 @@
   val is_theory_load: string -> bool
   val is_theory: string -> bool
   val is_proof: string -> bool
+  val is_proof_body: string -> bool
   val is_theory_goal: string -> bool
   val is_proof_goal: string -> bool
   val is_schematic_goal: string -> bool
@@ -230,10 +231,13 @@
 
 (* command categories *)
 
-fun command_category ks name =
-  (case command_keyword name of
-    NONE => false
-  | SOME k => member (op = o pairself kind_of) ks k);
+fun command_category ks =
+  let val tab = Symtab.make_set (map kind_of ks) in
+    fn name =>
+      (case command_keyword name of
+        NONE => false
+      | SOME k => Symtab.defined tab (kind_of k))
+  end;
 
 val is_diag = command_category [diag];
 val is_control = command_category [control];
@@ -256,6 +260,10 @@
     prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
     prf_asm, prf_asm_goal, prf_script];
 
+val is_proof_body = command_category
+  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+
 val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
 val is_schematic_goal = command_category [thy_schematic_goal];

--- a/src/Pure/Isar/outer_syntax.ML	Tue Feb 19 21:44:37 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Feb 20 00:00:42 2013 +0100
@@ -36,7 +36,7 @@
   val isar: TextIO.instream -> bool -> isar
   val span_cmts: Token.T list -> Token.T list
   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
-  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
+  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
 end;
 
@@ -331,13 +331,16 @@
       handle ERROR msg => (Toplevel.malformed proper_range msg, true)
   end;
 
-fun read_element outer_syntax init {head, proof, proper_proof} =
+fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
   let
     val read = read_span outer_syntax o Thy_Syntax.span_content;
     val (tr, proper_head) = read head |>> Toplevel.modify_init init;
-    val proof_trs = map read proof |> filter #2 |> map #1;
+    val proof_trs =
+      (case opt_proof of
+        NONE => []
+      | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
   in
-    if proper_head andalso proper_proof andalso
+    if proper_head andalso
       not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;

--- a/src/Pure/Thy/thy_syntax.ML	Tue Feb 19 21:44:37 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Feb 20 00:00:42 2013 +0100
@@ -15,8 +15,10 @@
   val span_content: span -> Token.T list
   val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
-  type element = {head: span, proof: span list, proper_proof: bool}
-  val parse_elements: span list -> element list
+  datatype 'a element = Element of 'a * ('a element list * 'a) option
+  val map_element: ('a -> 'b) -> 'a element -> 'b element
+  val flat_element: 'a element -> 'a list
+  val parse_elements: span list -> span element list
 end;
 
 structure Thy_Syntax: THY_SYNTAX =
@@ -134,10 +136,17 @@
 
 (** specification elements: commands with optional proof **)
 
-type element = {head: span, proof: span list, proper_proof: bool};
+datatype 'a element = Element of 'a * ('a element list * 'a) option;
+
+fun element (a, b) = Element (a, SOME b);
+fun atom a = Element (a, NONE);
 
-fun make_element head proof proper_proof =
-  {head = head, proof = proof, proper_proof = proper_proof};
+fun map_element f (Element (a, NONE)) = Element (f a, NONE)
+  | map_element f (Element (a, SOME (elems, b))) =
+      Element (f a, SOME ((map o map_element) f elems, f b));
+
+fun flat_element (Element (a, NONE)) = [a]
+  | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
 
 
 (* scanning spans *)
@@ -159,24 +168,21 @@
 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 Keyword.is_qed_global >> pair ~1 ||
-    command_with Keyword.is_proof_goal >> pair (d + 1) ||
-    (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
-    Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
+val proof_atom =
+  Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
 
-val element =
-  command_with Keyword.is_theory_goal -- proof
-    >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
-  Scan.one not_eof >> (fn a => make_element a [] true);
+fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
+and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
+
+val other_element =
+  command_with Keyword.is_theory_goal -- proof_rest >> element ||
+  Scan.one not_eof >> atom;
 
 in
 
 val parse_elements =
   Source.of_list #>
-  Source.source stopper (Scan.bulk element) NONE #>
+  Source.source stopper (Scan.bulk other_element) NONE #>
   Source.exhaust;
 
 end;