# HG changeset patch
# User aspinall
# Date 1172670381 -3600
# Node ID db0b80b8371ce885cb16aff6a27a4959b3e53df0
# Parent  c6002b06e63e8a925cffc3212a270646ad14b1a9
Add closeblock/openblock structure to proof-block commands

diff -r c6002b06e63e -r db0b80b8371c src/Pure/ProofGeneral/parsing.ML
--- a/src/Pure/ProofGeneral/parsing.ML	Wed Feb 28 13:33:10 2007 +0100
+++ b/src/Pure/ProofGeneral/parsing.ML	Wed Feb 28 14:46:21 2007 +0100
@@ -210,12 +210,11 @@
     (* proof control *)
     | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
     | "proof-heading"  => [D.Doccomment {text=str}]
-
-    | "proof-goal"     => (* nested proof: have, show, ... *)
-      [D.Opengoal {text=str,thmname=NONE}, 
-       D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
-			  
-    | "proof-block"    => [D.Proofstep {text=str}]
+    | "proof-goal"     => [D.Opengoal {text=str,thmname=NONE}, 
+			   D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
+    | "proof-block"    => [D.Closeblock {}, 
+			   D.Proofstep {text=str},
+			   D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
     | "proof-open"     => [D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}, 
 			   D.Proofstep {text=str} ]
     | "proof-close"    => [D.Proofstep {text=str}, D.Closeblock {}]