# HG changeset patch # User aspinall # Date 1165352664 -3600 # Node ID 01b2d13153c8c608efb98480fcdecea8e14c2b94 # Parent a6e25644b8456cea443517bdeb2ef6e76aae96a5 Document structure in pgip_markup.ML. Minor fixes. diff -r a6e25644b845 -r 01b2d13153c8 src/Pure/ProofGeneral/parsing.ML --- a/src/Pure/ProofGeneral/parsing.ML Tue Dec 05 19:33:15 2006 +0100 +++ b/src/Pure/ProofGeneral/parsing.ML Tue Dec 05 22:04:24 2006 +0100 @@ -7,7 +7,7 @@ signature PGIP_PARSER = sig - val xmls_of_str: string -> XML.tree list + val xmls_of_str: string -> XML.content end structure PgipParser : PGIP_PARSER = @@ -228,7 +228,7 @@ | "qed" => xmls_of_qed (name,markup) | "qed-block" => xmls_of_qed (name,markup) | "qed-global" => xmls_of_qed (name,markup) - | other => (* default for anything else is "spuriouscmd", ignored for undo. *) + | other => (* default for anything else is "spuriouscmd", ignored for undo *) (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other); markup "spuriouscmd") end diff -r a6e25644b845 -r 01b2d13153c8 src/Pure/ProofGeneral/pgip_input.ML --- a/src/Pure/ProofGeneral/pgip_input.ML Tue Dec 05 19:33:15 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_input.ML Tue Dec 05 22:04:24 2006 +0100 @@ -206,9 +206,11 @@ (* We allow sending proper document markup too; we map it back to dostep *) (* and strip out metainfo elements. Markup correctness isn't checked: this *) (* is a compatibility measure to make it easy for interfaces. *) - | "metainfo" => raise NoAction - | x => if (x mem PgipMarkup.markup_elements) - then Dostep { text = xmltext data } (* could use Doitem too *) + | x => if (x mem PgipMarkup.doc_markup_elements) then + if (x mem PgipMarkup.doc_markup_elements_ignored) then + raise NoAction + else + Dostep { text = xmltext data } (* could separate out Doitem too *) else raise Unknown) handle Unknown => NONE | NoAction => NONE end diff -r a6e25644b845 -r 01b2d13153c8 src/Pure/ProofGeneral/pgip_markup.ML --- a/src/Pure/ProofGeneral/pgip_markup.ML Tue Dec 05 19:33:15 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_markup.ML Tue Dec 05 22:04:24 2006 +0100 @@ -7,14 +7,158 @@ signature PGIPMARKUP = sig - val markup_elements : string list + (* Generic markup on sequential, non-overlapping pieces of proof text *) + datatype pgipdoc = + Openblock of { metavarid: string option } + | Closeblock of { } + | Opentheory of { thyname: string option, parentnames: string list , text: string} + | Theoryitem of { name: string option, objtype: string option, text: string } + | Closetheory of { text: string } + | Opengoal of { thmname: string option, text: string } + | Proofstep of { text: string } + | Closegoal of { text: string } + | Giveupgoal of { text: string } + | Postponegoal of { text: string } + | Comment of { text: string } + | Doccomment of { text: string } + | Whitespace of { text: string } + | Spuriouscmd of { text: string } + | Badcmd of { text: string } + | Metainfo of { name: string option, text: string } + (* Last three for PGIP literate markup only: *) + | Litcomment of { format: string option, content: XML.content } + | Showcode of { show: bool } + | Setformat of { format: string } + + type pgipdocument = pgipdoc list + type pgip_parser = string -> pgipdocument (* system must provide a parser P *) + val unparse_doc : pgipdocument -> string list (* s.t. unparse (P x) = x *) + val output_doc : pgipdocument -> XML.content + val doc_markup_elements : string list (* used in pgip_input *) + val doc_markup_elements_ignored : string list (* used in pgip_input *) end + structure PgipMarkup : PGIPMARKUP = struct + open PgipTypes + + datatype pgipdoc = + Openblock of { metavarid: string option } + | Closeblock of { } + | Opentheory of { thyname: string option, parentnames: string list , text: string} + | Theoryitem of { name: string option, objtype: string option, text: string } + | Closetheory of { text: string } + | Opengoal of { thmname: string option, text: string } + | Proofstep of { text: string } + | Closegoal of { text: string } + | Giveupgoal of { text: string } + | Postponegoal of { text: string } + | Comment of { text: string } + | Doccomment of { text: string } + | Whitespace of { text: string } + | Spuriouscmd of { text: string } + | Badcmd of { text: string } + | Metainfo of { name: string option, text: string } + | Litcomment of { format: string option, content: XML.content } + | Showcode of { show: bool } + | Setformat of { format: string } + + type pgipdocument = pgipdoc list + type pgip_parser = string -> pgipdocument + + fun xml_of docelt = + case docelt of + + Openblock vs => + XML.Elem("openblock", opt_attr "metavarid" (#metavarid vs), []) + + | Closeblock vs => + XML.Elem("closeblock", [], []) + + | Theoryitem vs => + XML.Elem("theoryitem", + opt_attr "name" (#name vs) @ + opt_attr "objtype" (#objtype vs), + [XML.Text (#text vs)]) + + | Closetheory vs => + XML.Elem("closetheory", [], [XML.Text (#text vs)]) + + | Opengoal vs => + XML.Elem("opengoal", + opt_attr "thmname" (#thmname vs), + [XML.Text (#text vs)]) + + | Proofstep vs => + XML.Elem("proofstep", [], [XML.Text (#text vs)]) + + | Closegoal vs => + XML.Elem("closegoal", [], [XML.Text (#text vs)]) + + | Giveupgoal vs => + XML.Elem("giveupgoal", [], [XML.Text (#text vs)]) + + | Postponegoal vs => + XML.Elem("postponegoal", [], [XML.Text (#text vs)]) + + | Comment vs => + XML.Elem("comment", [], [XML.Text (#text vs)]) + + | Doccomment vs => + XML.Elem("doccomment", [], [XML.Text (#text vs)]) + + | Spuriouscmd vs => + XML.Elem("spuriouscmd", [], [XML.Text (#text vs)]) + + | Badcmd vs => + XML.Elem("badcmd", [], [XML.Text (#text vs)]) + + | Metainfo vs => + XML.Elem("metainfo", opt_attr "name" (#name vs), + [XML.Text (#text vs)]) + + | Litcomment vs => + XML.Elem("litcomment", opt_attr "format" (#format vs), + #content vs) + + | Showcode vs => + XML.Elem("showcode", + attr "show" (PgipTypes.bool_to_pgstring (#show vs)), []) + + | Setformat vs => + XML.Elem("setformat", attr "format" (#format vs), []) + + val output_doc = map xml_of + + fun unparse_elt docelt = + case docelt of + Openblock vs => "" + | Closeblock vs => "" + | Opentheory vs => #text vs + | Theoryitem vs => #text vs + | Closetheory vs => #text vs + | Opengoal vs => #text vs + | Proofstep vs => #text vs + | Closegoal vs => #text vs + | Giveupgoal vs => #text vs + | Postponegoal vs => #text vs + | Comment vs => #text vs + | Doccomment vs => #text vs + | Whitespace vs => #text vs + | Spuriouscmd vs => #text vs + | Badcmd vs => #text vs + | Metainfo vs => #text vs + | _ => "" + + + val unparse_doc = map unparse_elt + + (* Names of all PGIP document markup elements *) - val markup_elements = - [ + val doc_markup_elements = + ["openblock", + "closeblock", "opengoal", "proofstep", "closegoal", @@ -27,7 +171,15 @@ "opentheory", "theoryitem", "closetheory", - "metainfo" (* non-document text *) - ] + "metainfo", + (* the prover should never receive the next three, + but we include them here so that they are ignored. *) + "litcomment", + "showcode", + "setformat"] + (* non-document/empty text, must be ignored *) + val doc_markup_elements_ignored = + [ "metainfo", "openblock", "closeblock", + "litcomment", "showcode", "setformat" ] end diff -r a6e25644b845 -r 01b2d13153c8 src/Pure/ProofGeneral/pgip_output.ML --- a/src/Pure/ProofGeneral/pgip_output.ML Tue Dec 05 19:33:15 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_output.ML Tue Dec 05 22:04:24 2006 +0100 @@ -13,17 +13,17 @@ | Normalresponse of { area: PgipTypes.displayarea, urgent: bool, messagecategory: PgipTypes.messagecategory, - content: XML.tree list } + content: XML.content } | Errorresponse of { fatality: PgipTypes.fatality, area: PgipTypes.displayarea option, location: PgipTypes.location option, - content: XML.tree list } + content: XML.content } | Informfileloaded of { url: PgipTypes.pgipurl } | Informfileretracted of { url: PgipTypes.pgipurl } - | Proofstate of { pgml: XML.tree list } + | Proofstate of { pgml: XML.content } | Metainforesponse of { attrs: XML.attributes, - content: XML.tree list } - | Lexicalstructure of { content: XML.tree list } + content: XML.content } + | Lexicalstructure of { content: XML.content } | Proverinfo of { name: string, version: string, instance: string, @@ -33,18 +33,18 @@ | Idtable of { objtype: string, context: string option, ids: string list } - | Setids of { idtables: XML.tree list } - | Delids of { idtables: XML.tree list } - | Addids of { idtables: XML.tree list } + | Setids of { idtables: XML.content } + | Delids of { idtables: XML.content } + | Addids of { idtables: XML.content } | Hasprefs of { prefcategory: string option, prefs: PgipTypes.preference list } | Prefval of { name: string, value: string } - | Idvalue of { name: string, objtype: string, text: XML.tree list } + | Idvalue of { name: string, objtype: string, text: XML.content } | Informguise of { file : PgipTypes.pgipurl option, theory: string option, theorem: string option, proofpos: int option } - | Parseresult of { attrs: XML.attributes, content: XML.tree list } + | Parseresult of { attrs: XML.attributes, content: XML.content } | Usespgip of { version: string, pgipelems: (string * bool * string list) list } | Usespgml of { version: string } @@ -54,7 +54,7 @@ destid: string option, refid: string option, refseq: int option, - content: XML.tree list } + content: XML.content } | Ready of { } val output : pgipoutput -> XML.tree @@ -67,26 +67,26 @@ datatype pgipoutput = Cleardisplay of { area: displayarea } | Normalresponse of { area: displayarea, urgent: bool, - messagecategory: messagecategory, content: XML.tree list } + messagecategory: messagecategory, content: XML.content } | Errorresponse of { area: displayarea option, fatality: fatality, - location: location option, content: XML.tree list } + location: location option, content: XML.content } | Informfileloaded of { url: Path.T } | Informfileretracted of { url: Path.T } - | Proofstate of { pgml: XML.tree list } - | Metainforesponse of { attrs: XML.attributes, content: XML.tree list } - | Lexicalstructure of { content: XML.tree list } + | Proofstate of { pgml: XML.content } + | Metainforesponse of { attrs: XML.attributes, content: XML.content } + | Lexicalstructure of { content: XML.content } | Proverinfo of { name: string, version: string, instance: string, descr: string, url: Url.T, filenameextns: string } | Idtable of { objtype: string, context: string option, ids: string list } - | Setids of { idtables: XML.tree list } - | Delids of { idtables: XML.tree list } - | Addids of { idtables: XML.tree list } + | Setids of { idtables: XML.content } + | Delids of { idtables: XML.content } + | Addids of { idtables: XML.content } | Hasprefs of { prefcategory: string option, prefs: preference list } | Prefval of { name: string, value: string } - | Idvalue of { name: string, objtype: string, text: XML.tree list } + | Idvalue of { name: string, objtype: string, text: XML.content } | Informguise of { file : pgipurl option, theory: string option, theorem: string option, proofpos: int option } - | Parseresult of { attrs: XML.attributes, content: XML.tree list } + | Parseresult of { attrs: XML.attributes, content: XML.content } | Usespgip of { version: string, pgipelems: (string * bool * string list) list } | Usespgml of { version: string } @@ -96,7 +96,7 @@ destid: string option, refid: string option, refseq: int option, - content: XML.tree list} + content: XML.content } | Ready of { } @@ -231,7 +231,7 @@ fun async_attrs b = if b then attr "async" "true" else [] fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs) fun singlepgipelem (e,async,attrs) = - XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[]) + XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e]) in XML.Elem ("acceptedpgipelems", [], diff -r a6e25644b845 -r 01b2d13153c8 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Dec 05 19:33:15 2006 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Dec 05 22:04:24 2006 +0100 @@ -320,6 +320,7 @@ tell_clear_goals (); tell_clear_response (); welcome (); + priority "Running new version of PGIP code. In testing."; raise Toplevel.RESTART) @@ -847,19 +848,21 @@ (let val class = PgipTypes.get_attr "class" attrs val dest = PgipTypes.get_attr_opt "destid" attrs - val _ = (pgip_refid := PgipTypes.get_attr_opt "id" attrs) - val _ = (pgip_refseq := Option.join - (Option.map Int.fromString - (PgipTypes.get_attr_opt "seq" attrs))) + val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs) (* Respond to prover broadcasts, or messages for us. Ignore rest *) val processit = case dest of NONE => class = "pa" | SOME id => matching_pgip_id id - in - if processit then - (List.app process_pgip_element pgips; true) - else false + in if processit then + (pgip_refid := PgipTypes.get_attr_opt "id" attrs; + pgip_refseq := SOME seq; + List.app process_pgip_element pgips; + (* return true to indicate *) + true) + else + (* no response to ignored messages. *) + false end) | _ => raise PGIP "Invalid PGIP packet received") handle PGIP msg =>