diff -r 790935f7c1ab -r 7eef90be0db4 src/Pure/ProofGeneral/parsing.ML --- a/src/Pure/ProofGeneral/parsing.ML Sat Mar 03 12:39:50 2007 +0100 +++ b/src/Pure/ProofGeneral/parsing.ML Sat Mar 03 12:42:04 2007 +0100 @@ -20,6 +20,8 @@ structure P = OuterParse; structure D = PgipMarkup; +structure I = PgipIsabelle; +structure T = PgipTypes; (* Notes. This is quite tricky, because 1) we need to put back whitespace which @@ -85,7 +87,7 @@ fun nameparse elt objtyp nameP toks = (fst (nameP (toks@sync))) handle _ => (error ("Error occurred in name parser for " ^ elt ^ - "(objtype: " ^ objtyp ^ ")"); + "(objtype: " ^ (T.name_of_objtype objtyp) ^ ")"); "") fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg) @@ -96,7 +98,8 @@ in [D.Opentheory { thyname=thyname, parentnames = imports, - text = str }] + text = str }, + D.Openblock { metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody }] end fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *) @@ -119,7 +122,9 @@ "declare"] fun named_item nameP ty = - [D.Theoryitem {text=str,name=SOME (nameparse "theoryitem" ty nameP toks),objtype=SOME ty}] + [D.Theoryitem {text=str, + name=SOME (nameparse "theoryitem" ty nameP toks), + objtype=SOME ty}] val plain_item = [D.Theoryitem {text=str,name=NONE,objtype=NONE}] val doccomment = @@ -145,18 +150,19 @@ else case name of "text" => doccomment | "text_raw" => doccomment - | "typedecl" => named_item (P.type_args |-- P.name) "type" - | "types" => named_item (P.type_args |-- P.name) "type" - | "classes" => named_item P.name "class" - | "classrel" => named_item P.name "class" - | "consts" => named_item (P.const >> #1) "term" - | "axioms" => named_item (SpecParse.spec_name >> (#1 o #1)) "theorem" - | "defs" => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) "theorem" - | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term" - | "theorems" => named_item thmnameP "thmset" - | "lemmas" => named_item thmnameP "thmset" - | "oracle" => named_item P.name "oracle" - | "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale" + | "typedecl" => named_item (P.type_args |-- P.name) T.ObjType + | "types" => named_item (P.type_args |-- P.name) T.ObjType + | "classes" => named_item P.name I.ObjClass + | "classrel" => named_item P.name I.ObjClass + | "consts" => named_item (P.const >> #1) T.ObjTerm + | "axioms" => named_item (SpecParse.spec_name >> (#1 o #1)) T.ObjTheorem + | "defs" => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) T.ObjTheorem + | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) T.ObjTerm + | "theorems" => named_item thmnameP I.ObjTheoremSet + | "lemmas" => named_item thmnameP I.ObjTheoremSet + | "oracle" => named_item P.name I.ObjOracle + (* FIXME: locale needs to introduce a block *) + | "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) I.ObjLocale | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item) end @@ -175,10 +181,10 @@ fst a) (* a : (bstring * Args.src list) *) val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "") - val thmname = nameparse "opengoal" "theorem" nameP toks + val thmname = nameparse "opengoal" T.ObjTheorem nameP toks in [D.Opengoal {thmname=SOME thmname, text=str}, - D.Openblock {metavarid=NONE,name=NONE,objtype=SOME "theorem-proof"}] + D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}] end fun xmls_of_qed (name,str) = @@ -204,28 +210,28 @@ (* theory/files *) | "theory-begin" => xmls_of_thy_begin (name,toks,str) | "theory-decl" => xmls_of_thy_decl (name,toks,str) - | "theory-heading" => [D.Doccomment {text=str}] - | "theory-script" => [D.Theoryitem {name=NONE,objtype=NONE,text=str}] - | "theory-end" => [D.Closetheory {text=str}] + | "theory-heading" => [D.Closeblock {}, + D.Doccomment {text=str}, + D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody}] + | "theory-script" => [D.Theoryitem {name=NONE,objtype=SOME I.ObjTheoryDecl,text=str}] + | "theory-end" => [D.Closeblock {}, D.Closetheory {text=str}] (* proof control *) | "theory-goal" => xmls_of_thy_goal (name,toks,str) | "proof-heading" => [D.Doccomment {text=str}] | "proof-goal" => [D.Opengoal {text=str,thmname=NONE}, - D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] + D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}] | "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.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}] + | "proof-open" => [D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}, D.Proofstep {text=str} ] | "proof-close" => [D.Proofstep {text=str}, D.Closeblock {}] | "proof-script" => [D.Proofstep {text=str}] | "proof-chain" => [D.Proofstep {text=str}] | "proof-decl" => [D.Proofstep {text=str}] | "proof-asm" => [D.Proofstep {text=str}] - | "proof-asm-goal" => (* nested proof: obtain, ... *) - [D.Opengoal {text=str,thmname=NONE}, - D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] - + | "proof-asm-goal" => [D.Opengoal {text=str,thmname=NONE}, + D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] | "qed" => xmls_of_qed (name,str) | "qed-block" => xmls_of_qed (name,str) | "qed-global" => xmls_of_qed (name,str)