Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add closeblock/openblock structure to proof-block commands
authoraspinall
Wed, 28 Feb 2007 14:46:21 +0100
changeset 22374 db0b80b8371c
parent 22373 c6002b06e63e
child 22375 823f7bee42df
Add closeblock/openblock structure to proof-block commands
src/Pure/ProofGeneral/parsing.ML file | annotate | diff | comparison | revisions 
--- 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 {}]
isabelle