Document structure in pgip_markup.ML. Minor fixes.
--- 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
--- 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
--- 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
--- 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", [],
--- 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 <ready/> *)
+ true)
+ else
+ (* no response to ignored messages. *)
+ false
end)
| _ => raise PGIP "Invalid PGIP packet received")
handle PGIP msg =>