# HG changeset patch
# User aspinall
# Date 1096737736 -7200
# Node ID 68ab0f4eb45708d8f3b518e9e1cf7c4a1426e172
# Parent  1bd35fd87963cd399efb65bfbc4638ee97c0af67
Add openblock/closeblock to other opengoal/closegoal elements

diff -r 1bd35fd87963 -r 68ab0f4eb457 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Oct 01 11:55:43 2004 +0200
+++ b/src/Pure/proof_general.ML	Sat Oct 02 19:22:16 2004 +0200
@@ -709,7 +709,7 @@
    was removed during parsing so we can provide markup around commands;
    2) parsing is intertwined with execution in Isar so we have to repeat
    the parsing to extract interesting parts of commands.  The trace of
-   tokens parsed which is now recorded in each transition helps to do this.
+   tokens parsed which is now recorded in each transition helps do this.
    
    If we had proper parse trees it would be easy, or if we could go
    beyond ML's type system to allow existential types to be part of
@@ -837,8 +837,8 @@
 	end
 
     fun xmls_of_thy_goal (name,toks,str) = 
-     let 
-	 (* see isar_syn.ML/gen_theorem *)
+	let 
+	    (* see isar_syn.ML/gen_theorem *)
          val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
 	 val general_statement =
 	    statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
@@ -853,11 +853,12 @@
 	    (* TODO: add preference values for attributes 
 	       val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
 	    *)
-     in 
-	 thmnamed_item_elt toks str "opengoal" nameP ""
-     end
+	in 
+	    (thmnamed_item_elt toks str "opengoal" nameP "") @
+	    (empty "openblock")
+	end
 
-    fun xmls_of_qed (name,markup) = case name of
+    fun xmls_of_qed (name,markup) = (case name of
       "sorry"         => markup "giveupgoal"
     | "oops"          => markup "postponegoal"
     | "done"          => markup "closegoal" 
@@ -866,7 +867,8 @@
     | "."	      => markup "closegoal"  (* nested or toplevel *)
     | ".."	      => markup "closegoal"  (* nested or toplevel *)
     | other => (* default to closegoal: may be wrong for extns *)
-      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal")
+      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal"))
+	@ (empty "closeblock")
 
     fun xmls_of_kind kind (name,toks,str) = 
     let val markup = markup_text str in 
@@ -882,7 +884,7 @@
     (* proof control *)
     | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
     | "proof-heading"  => markup "litcomment"
-    | "proof-goal"     => markup "opengoal"  (* nested proof: have, show, ... *)
+    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
     | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
     | "proof-open"     => (empty "openblock") @ (markup "proofstep")
     | "proof-close"    => (markup "proofstep") @ (empty "closeblock")