Add openblock/closeblock to other opengoal/closegoal elements
authoraspinall
Sat Oct 02 19:22:16 2004 +0200 (2004-10-02)
changeset 1522568ab0f4eb457
parent 15224 1bd35fd87963
child 15226 df9b45e9a39f
Add openblock/closeblock to other opengoal/closegoal elements
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Oct 01 11:55:43 2004 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Sat Oct 02 19:22:16 2004 +0200
     1.3 @@ -709,7 +709,7 @@
     1.4     was removed during parsing so we can provide markup around commands;
     1.5     2) parsing is intertwined with execution in Isar so we have to repeat
     1.6     the parsing to extract interesting parts of commands.  The trace of
     1.7 -   tokens parsed which is now recorded in each transition helps to do this.
     1.8 +   tokens parsed which is now recorded in each transition helps do this.
     1.9     
    1.10     If we had proper parse trees it would be easy, or if we could go
    1.11     beyond ML's type system to allow existential types to be part of
    1.12 @@ -837,8 +837,8 @@
    1.13  	end
    1.14  
    1.15      fun xmls_of_thy_goal (name,toks,str) = 
    1.16 -     let 
    1.17 -	 (* see isar_syn.ML/gen_theorem *)
    1.18 +	let 
    1.19 +	    (* see isar_syn.ML/gen_theorem *)
    1.20           val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
    1.21  	 val general_statement =
    1.22  	    statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
    1.23 @@ -853,11 +853,12 @@
    1.24  	    (* TODO: add preference values for attributes 
    1.25  	       val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
    1.26  	    *)
    1.27 -     in 
    1.28 -	 thmnamed_item_elt toks str "opengoal" nameP ""
    1.29 -     end
    1.30 +	in 
    1.31 +	    (thmnamed_item_elt toks str "opengoal" nameP "") @
    1.32 +	    (empty "openblock")
    1.33 +	end
    1.34  
    1.35 -    fun xmls_of_qed (name,markup) = case name of
    1.36 +    fun xmls_of_qed (name,markup) = (case name of
    1.37        "sorry"         => markup "giveupgoal"
    1.38      | "oops"          => markup "postponegoal"
    1.39      | "done"          => markup "closegoal" 
    1.40 @@ -866,7 +867,8 @@
    1.41      | "."	      => markup "closegoal"  (* nested or toplevel *)
    1.42      | ".."	      => markup "closegoal"  (* nested or toplevel *)
    1.43      | other => (* default to closegoal: may be wrong for extns *)
    1.44 -      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal")
    1.45 +      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal"))
    1.46 +	@ (empty "closeblock")
    1.47  
    1.48      fun xmls_of_kind kind (name,toks,str) = 
    1.49      let val markup = markup_text str in 
    1.50 @@ -882,7 +884,7 @@
    1.51      (* proof control *)
    1.52      | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
    1.53      | "proof-heading"  => markup "litcomment"
    1.54 -    | "proof-goal"     => markup "opengoal"  (* nested proof: have, show, ... *)
    1.55 +    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
    1.56      | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
    1.57      | "proof-open"     => (empty "openblock") @ (markup "proofstep")
    1.58      | "proof-close"    => (markup "proofstep") @ (empty "closeblock")