--- a/src/Pure/ProofGeneral/pgip_input.ML Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML Thu Apr 03 21:23:39 2008 +0200
@@ -63,7 +63,7 @@
(* unofficial escape command for debugging *)
| Quitpgip of { }
- val input : XML.element -> pgipinput option (* raises PGIP *)
+ val input: string * XML.attributes * XML.tree list -> pgipinput option (* raises PGIP *)
end
structure PgipInput : PGIPINPUT =
--- a/src/Pure/ProofGeneral/pgip_markup.ML Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Thu Apr 03 21:23:39 2008 +0200
@@ -28,14 +28,14 @@
| Unparseable 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 }
+ | Litcomment of { format: string option, content: XML.tree list }
| 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 output_doc : pgipdocument -> XML.tree list
val doc_markup_elements : string list (* used in pgip_input *)
val doc_markup_elements_ignored : string list (* used in pgip_input *)
end
@@ -65,7 +65,7 @@
| Badcmd of { text: string }
| Unparseable of { text: string }
| Metainfo of { name: string option, text: string }
- | Litcomment of { format: string option, content: XML.content }
+ | Litcomment of { format: string option, content: XML.tree list }
| Showcode of { show: bool }
| Setformat of { format: string }
--- a/src/Pure/ProofGeneral/pgip_output.ML Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML Thu Apr 03 21:23:39 2008 +0200
@@ -9,16 +9,16 @@
sig
(* These are the PGIP messages which the prover emits. *)
datatype pgipoutput =
- Normalresponse of { content: XML.content }
+ Normalresponse of { content: XML.tree list }
| Errorresponse of { fatality: PgipTypes.fatality,
location: PgipTypes.location option,
- content: XML.content }
+ content: XML.tree list }
| Informfileloaded of { url: PgipTypes.pgipurl, completed: bool }
| Informfileoutdated of { url: PgipTypes.pgipurl, completed: bool }
| Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
| Metainforesponse of { attrs: XML.attributes,
- content: XML.content }
- | Lexicalstructure of { content: XML.content }
+ content: XML.tree list }
+ | Lexicalstructure of { content: XML.tree list }
| Proverinfo of { name: string,
version: string,
instance: string,
@@ -40,13 +40,13 @@
| Idvalue of { thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype,
name: PgipTypes.objname,
- text: XML.content }
+ text: XML.tree list }
| Informguise of { file : PgipTypes.pgipurl option,
theory: PgipTypes.objname option,
theorem: PgipTypes.objname option,
proofpos: int option }
| Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument,
- errs: XML.content } (* errs to become PGML *)
+ errs: XML.tree list } (* errs to become PGML *)
| Usespgip of { version: string,
pgipelems: (string * bool * string list) list }
| Usespgml of { version: string }
@@ -56,7 +56,7 @@
destid: string option,
refid: string option,
refseq: int option,
- content: XML.content }
+ content: XML.tree list }
| Ready of { }
val output : pgipoutput -> XML.tree
@@ -67,15 +67,15 @@
open PgipTypes
datatype pgipoutput =
- Normalresponse of { content: XML.content }
+ Normalresponse of { content: XML.tree list }
| Errorresponse of { fatality: fatality,
location: location option,
- content: XML.content }
+ content: XML.tree list }
| Informfileloaded of { url: Path.T, completed: bool }
| Informfileoutdated of { url: Path.T, completed: bool }
| Informfileretracted of { url: Path.T, completed: bool }
- | Metainforesponse of { attrs: XML.attributes, content: XML.content }
- | Lexicalstructure of { content: XML.content }
+ | Metainforesponse of { attrs: XML.attributes, content: XML.tree list }
+ | Lexicalstructure of { content: XML.tree list }
| Proverinfo of { name: string, version: string, instance: string,
descr: string, url: Url.T, filenameextns: string }
| Setids of { idtables: PgipTypes.idtable list }
@@ -86,7 +86,7 @@
| Idvalue of { thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype,
name: PgipTypes.objname,
- text: XML.content }
+ text: XML.tree list }
| Setrefs of { url: PgipTypes.pgipurl option,
thyname: PgipTypes.objname option,
objtype: PgipTypes.objtype option,
@@ -98,7 +98,7 @@
theorem: PgipTypes.objname option,
proofpos: int option }
| Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
- errs: XML.content } (* errs to become PGML *)
+ errs: XML.tree list } (* errs to become PGML *)
| Usespgip of { version: string,
pgipelems: (string * bool * string list) list }
| Usespgml of { version: string }
@@ -108,7 +108,7 @@
destid: string option,
refid: string option,
refseq: int option,
- content: XML.content }
+ content: XML.tree list }
| Ready of { }
--- a/src/Pure/ProofGeneral/pgml.ML Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML Thu Apr 03 21:23:39 2008 +0200
@@ -33,7 +33,7 @@
xref: PgipTypes.pgipurl option,
content: pgmlterm list }
| Alt of { kind: string option, content: pgmlterm list }
- | Embed of XML.content
+ | Embed of XML.tree list
| Raw of XML.tree
datatype pgml =
@@ -77,7 +77,7 @@
xref: PgipTypes.pgipurl option,
content: pgmlterm list }
| Alt of { kind: string option, content: pgmlterm list }
- | Embed of XML.content
+ | Embed of XML.tree list
| Raw of XML.tree
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 03 21:23:39 2008 +0200
@@ -1115,7 +1115,7 @@
in
(* TODO: add socket interface *)
- val xmlP = XML.parse_comment_whspc |-- XML.parse_elem >> single
+ val xmlP = XML.parse_comment_whspc |-- XML.parse_element >> single
val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)