--- a/src/Pure/proof_general.ML Wed Nov 22 20:51:00 2006 +0100
+++ b/src/Pure/proof_general.ML Thu Nov 23 00:09:24 2006 +0100
@@ -869,7 +869,7 @@
"declare"]
val plain_item = markup_text str "theoryitem"
- val comment_item = markup_text str "litcomment"
+ val comment_item = markup_text str "doccomment"
val named_item = named_item_elt toks str "theoryitem"
val opt_overloaded = P.opt_keyword "overloaded";
@@ -953,12 +953,12 @@
(* theory/files *)
| "theory-begin" => xmls_of_thy_begin (name,toks,str)
| "theory-decl" => xmls_of_thy_decl (name,toks,str)
- | "theory-heading" => markup "litcomment"
+ | "theory-heading" => markup "doccomment"
| "theory-script" => markup "theorystep"
| "theory-end" => markup "closetheory"
(* proof control *)
| "theory-goal" => xmls_of_thy_goal (name,toks,str)
- | "proof-heading" => markup "litcomment"
+ | "proof-heading" => markup "doccomment"
| "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")
@@ -1022,7 +1022,7 @@
(if (length rest2 = length rest1) then []
else markup_text (implode
(map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
- "litcomment") @
+ "doccomment") @
(markup_comment_whs postwhs),
Library.take (length rest3 - 1,rest3))
end
@@ -1259,9 +1259,10 @@
| "closegoal" => isarscript data
| "giveupgoal" => isarscript data
| "postponegoal" => isarscript data
- | "comment" => isarscript data (* NB: should be ignored, but process anyway *)
+ | "comment" => isarscript data
+ | "doccomment" => isarscript data
| "whitespace" => isarscript data (* NB: should be ignored, but process anyway *)
- | "litcomment" => isarscript data
+ | "litcomment" => isarscript data (* NB: should be ignored, process for back compat *)
| "spuriouscmd" => isarscript data
| "badcmd" => isarscript data
(* improperproofcmd: improper commands which *do not* belong in script *)