--- 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")