--- a/src/Pure/ProofGeneral/pgip_input.ML Mon May 13 20:35:04 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,239 +0,0 @@
-(* Title: Pure/ProofGeneral/pgip_input.ML
- Author: David Aspinall
-
-PGIP abstraction: input commands.
-*)
-
-signature PGIPINPUT =
-sig
- (* These are the PGIP commands to which we respond. *)
- datatype pgipinput =
- (* protocol/prover config *)
- Askpgip of { }
- | Askpgml of { }
- | Askconfig of { }
- | Askprefs of { }
- | Setpref of { name:string, prefcategory:string option, value:string }
- | Getpref of { name:string, prefcategory:string option }
- (* prover control *)
- | Proverinit of { }
- | Proverexit of { }
- | Setproverflag of { flagname:string, value: bool }
- (* improper proof commands: control proof state *)
- | Dostep of { text: string }
- | Undostep of { times: int }
- | Redostep of { }
- | Abortgoal of { }
- | Forget of { thyname: string option, name: string option,
- objtype: PgipTypes.objtype option }
- | Restoregoal of { thmname : string }
- (* context inspection commands *)
- | Askids of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option }
- | Askrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option }
- | Showid of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname }
- | Askguise of { }
- | Parsescript of { text: string, location: PgipTypes.location,
- systemdata: string option }
- | Showproofstate of { }
- | Showctxt of { }
- | Searchtheorems of { arg: string }
- | Setlinewidth of { width: int }
- | Viewdoc of { arg: string }
- (* improper theory-level commands *)
- | Doitem of { text: string }
- | Undoitem of { }
- | Redoitem of { }
- | Aborttheory of { }
- | Retracttheory of { thyname: string }
- | Loadfile of { url: PgipTypes.pgipurl }
- | Openfile of { url: PgipTypes.pgipurl }
- | Closefile of { }
- | Abortfile of { }
- | Retractfile of { url: PgipTypes.pgipurl }
- | Changecwd of { url: PgipTypes.pgipurl }
- | Systemcmd of { arg: string }
- (* unofficial escape command for debugging *)
- | Quitpgip of { }
-
- val input: Markup.T * XML.tree list -> pgipinput option (* raises PGIP *)
-end
-
-structure PgipInput : PGIPINPUT =
-struct
-
-open PgipTypes
-
-(*** PGIP input ***)
-
-datatype pgipinput =
- (* protocol/prover config *)
- Askpgip of { }
- | Askpgml of { }
- | Askconfig of { }
- | Askprefs of { }
- | Setpref of { name:string, prefcategory:string option, value:string }
- | Getpref of { name:string, prefcategory:string option }
- (* prover control *)
- | Proverinit of { }
- | Proverexit of { }
- | Setproverflag of { flagname:string, value: bool }
- (* improper proof commands: control proof state *)
- | Dostep of { text: string }
- | Undostep of { times: int }
- | Redostep of { }
- | Abortgoal of { }
- | Forget of { thyname: string option, name: string option,
- objtype: PgipTypes.objtype option }
- | Restoregoal of { thmname : string }
- (* context inspection commands *)
- | Askids of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option }
- | Askrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option }
- | Showid of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname }
- | Askguise of { }
- | Parsescript of { text: string, location: location,
- systemdata: string option }
- | Showproofstate of { }
- | Showctxt of { }
- | Searchtheorems of { arg: string }
- | Setlinewidth of { width: int }
- | Viewdoc of { arg: string }
- (* improper theory-level commands *)
- | Doitem of { text: string }
- | Undoitem of { }
- | Redoitem of { }
- | Aborttheory of { }
- | Retracttheory of { thyname: string }
- | Loadfile of { url: pgipurl }
- | Openfile of { url: pgipurl }
- | Closefile of { }
- | Abortfile of { }
- | Retractfile of { url: pgipurl }
- | Changecwd of { url: pgipurl }
- | Systemcmd of { arg: string }
- (* unofficial escape command for debugging *)
- | Quitpgip of { }
-
-(* Extracting content from input XML elements to make a PGIPinput *)
-local
-
- val thyname_attro = get_attr_opt "thyname"
- val thyname_attr = get_attr "thyname"
- val name_attr = get_attr "name"
- val name_attro = get_attr_opt "name"
- val thmname_attr = get_attr "thmname"
- val flagname_attr = get_attr "flagname"
- val value_attr = get_attr "value"
-
- fun objtype_attro attrs = if has_attr "objtype" attrs then
- SOME (objtype_of_attrs attrs)
- else NONE
-
- fun pgipurl_attro attrs = if has_attr "url" attrs then
- SOME (pgipurl_of_attrs attrs)
- else NONE
-
- val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
- val prefcat_attr = get_attr_opt "prefcategory"
-
- fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
- | xmltext [] = ""
- | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
-
- exception Unknown
- exception NoAction
-in
-
-(* Return a valid PGIP input command.
- Raise PGIP exception for invalid data.
- Return NONE for unknown/unhandled commands.
-*)
-fun input ((elem, attrs), data) =
-SOME
- (case elem of
- "askpgip" => Askpgip { }
- | "askpgml" => Askpgml { }
- | "askconfig" => Askconfig { }
- (* proverconfig *)
- | "askprefs" => Askprefs { }
- | "getpref" => Getpref { name = name_attr attrs,
- prefcategory = prefcat_attr attrs }
- | "setpref" => Setpref { name = name_attr attrs,
- prefcategory = prefcat_attr attrs,
- value = xmltext data }
- (* provercontrol *)
- | "proverinit" => Proverinit { }
- | "proverexit" => Proverexit { }
- | "setproverflag" => Setproverflag { flagname = flagname_attr attrs,
- value = read_pgipbool (value_attr attrs) }
- (* improperproofcmd: improper commands not in script *)
- | "dostep" => Dostep { text = xmltext data }
- | "undostep" => Undostep { times = times_attr attrs }
- | "redostep" => Redostep { }
- | "abortgoal" => Abortgoal { }
- | "forget" => Forget { thyname = thyname_attro attrs,
- name = name_attro attrs,
- objtype = objtype_attro attrs }
- | "restoregoal" => Restoregoal { thmname = thmname_attr attrs}
- (* proofctxt: improper commands *)
- | "askids" => Askids { url = pgipurl_attro attrs,
- thyname = thyname_attro attrs,
- objtype = objtype_attro attrs }
- | "askrefs" => Askrefs { url = pgipurl_attro attrs,
- thyname = thyname_attro attrs,
- objtype = objtype_attro attrs,
- name = name_attro attrs }
- | "showid" => Showid { thyname = thyname_attro attrs,
- objtype = objtype_of_attrs attrs,
- name = name_attr attrs }
- | "askguise" => Askguise { }
- | "parsescript" => Parsescript { text = (xmltext data),
- systemdata = get_attr_opt "systemdata" attrs,
- location = location_of_attrs attrs }
- | "showproofstate" => Showproofstate { }
- | "showctxt" => Showctxt { }
- | "searchtheorems" => Searchtheorems { arg = xmltext data }
- | "setlinewidth" => Setlinewidth { width = read_pgipnat (xmltext data) }
- | "viewdoc" => Viewdoc { arg = xmltext data }
- (* improperfilecmd: theory-level commands not in script *)
- | "doitem" => Doitem { text = xmltext data }
- | "undoitem" => Undoitem { }
- | "redoitem" => Redoitem { }
- | "aborttheory" => Aborttheory { }
- | "retracttheory" => Retracttheory { thyname = thyname_attr attrs }
- | "loadfile" => Loadfile { url = pgipurl_of_attrs attrs }
- | "openfile" => Openfile { url = pgipurl_of_attrs attrs }
- | "closefile" => Closefile { }
- | "abortfile" => Abortfile { }
- | "retractfile" => Retractfile { url = pgipurl_of_attrs attrs }
- | "changecwd" => Changecwd { url = pgipurl_of_attrs attrs }
- | "systemcmd" => Systemcmd { arg = xmltext data }
- (* unofficial command for debugging *)
- | "quitpgip" => Quitpgip { }
-
- (* 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. *)
- | x => if member (op =) PgipMarkup.doc_markup_elements x then
- if member (op =) PgipMarkup.doc_markup_elements_ignored x then
- raise NoAction
- else
- Dostep { text = xmltext data } (* could separate out Doitem too *)
- else raise Unknown)
- handle Unknown => NONE | NoAction => NONE
-end
-
-end
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Mon May 13 20:35:04 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: Pure/ProofGeneral/pgip_isabelle.ML
- Author: David Aspinall
-
-Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
-*)
-
-signature PGIP_ISABELLE =
-sig
- val isabelle_pgml_version_supported : string
- val isabelle_pgip_version_supported : string
- val systemid : string
- val accepted_inputs : (string * bool * (string list)) list
-
- val location_of_position : Position.T -> PgipTypes.location
-
- (* Additional types of objects in Isar scripts *)
-
- val ObjTheoryBody : PgipTypes.objtype
- val ObjTheoryDecl : PgipTypes.objtype
- val ObjTheoryBodySubsection : PgipTypes.objtype
- val ObjProofBody : PgipTypes.objtype
- val ObjFormalComment : PgipTypes.objtype
- val ObjClass : PgipTypes.objtype
- val ObjTheoremSet : PgipTypes.objtype
- val ObjOracle : PgipTypes.objtype
- val ObjLocale : PgipTypes.objtype
-
-end
-
-structure PgipIsabelle : PGIP_ISABELLE =
-struct
-
-val isabelle_pgml_version_supported = "2.0";
-val isabelle_pgip_version_supported = "2.0"
-val systemid = "Isabelle"
-
-
-(** Accepted commands **)
-
-local
-
- (* These element names are a subset of those in pgip_input.ML.
- They must be handled in proof_general_pgip.ML/process_pgip_element. *)
-
- val accepted_names =
- (* not implemented: "askconfig", "forget", "restoregoal" *)
- ["askpgip","askpgml","askprefs","getpref","setpref",
- "proverinit","proverexit","startquiet","stopquiet",
- "pgmlsymbolson", "pgmlsymbolsoff",
- "dostep", "undostep", "redostep", "abortgoal",
- "askids", "showid", "askguise",
- "parsescript",
- "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
- "doitem", "undoitem", "redoitem", "abortheory",
- "retracttheory", "loadfile", "openfile", "closefile",
- "abortfile", "retractfile", "changecwd", "systemcmd"];
-
- fun element_async p =
- false (* single threaded only *)
-
- fun supported_optional_attrs p = (case p of
- "undostep" => ["times"]
- (* TODO: we could probably extend these too:
- | "redostep" => ["times"]
- | "undoitem" => ["times"]
- | "redoitem" => ["times"] *)
- | _ => [])
-in
-val accepted_inputs =
- (map (fn p=> (p, element_async p, supported_optional_attrs p))
- accepted_names);
-end
-
-
-fun location_of_position pos =
- let val line = Position.line_of pos
- val (url,descr) =
- (case Position.file_of pos of
- NONE => (NONE, NONE)
- | SOME fname =>
- let val path = Path.explode fname in
- if File.exists path
- then (SOME (PgipTypes.pgipurl_of_path path), NONE)
- else (NONE, SOME fname)
- end);
- in
- { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
- end
-
-
-val [ObjTheoryBody,
- ObjTheoryDecl,
- ObjTheoryBodySubsection,
- ObjProofBody,
- ObjFormalComment,
- ObjClass,
- ObjTheoremSet,
- ObjOracle,
- ObjLocale] =
- map PgipTypes.ObjOther
- ["theory body",
- "theory declaration",
- "theory subsection",
- "proof body",
- "formal comment",
- "class",
- "theorem set declaration",
- "oracle",
- "locale"];
-
-end
--- a/src/Pure/ProofGeneral/pgip_markup.ML Mon May 13 20:35:04 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-(* Title: Pure/ProofGeneral/pgip_markup.ML
- Author: David Aspinall
-
-PGIP abstraction: document markup for proof scripts (in progress).
-*)
-
-signature PGIPMARKUP =
-sig
- (* Generic markup on sequential, non-overlapping pieces of proof text *)
- datatype pgipdoc =
- Openblock of { metavarid: string option, name: string option,
- objtype: PgipTypes.objtype option }
- | Closeblock of { }
- | Opentheory of { thyname: string option, parentnames: string list , text: string}
- | Theoryitem of { name: string option, objtype: PgipTypes.objtype 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 }
- | 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.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.tree list
- 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
-
-(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
- datatype pgipdoc =
- Openblock of { metavarid: string option, name: string option,
- objtype: PgipTypes.objtype option }
- | Closeblock of { }
- | Opentheory of { thyname: string option, parentnames: string list, text: string}
- | Theoryitem of { name: string option, objtype: PgipTypes.objtype 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 }
- | Unparseable of { text: string }
- | Metainfo of { name: string option, text: string }
- | 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
-
- fun xml_of docelt =
- case docelt of
-
- Openblock vs =>
- XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
- opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
- opt_attr "metavarid" (#metavarid vs)),
- [])
-
- | Closeblock _ =>
- XML.Elem(("closeblock", []), [])
-
- | Opentheory vs =>
- XML.Elem(("opentheory",
- opt_attr "thyname" (#thyname vs) @
- opt_attr "parentnames"
- (case (#parentnames vs)
- of [] => NONE
- | ps => SOME (space_implode ";" ps))),
- [XML.Text (#text vs)])
-
- | Theoryitem vs =>
- XML.Elem(("theoryitem",
- opt_attr "name" (#name vs) @
- opt_attr_map PgipTypes.name_of_objtype "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)])
-
- | Whitespace vs =>
- XML.Elem(("whitespace", []), [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)])
-
- | Unparseable vs =>
- XML.Elem(("unparseable", []), [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 _ => ""
- | Closeblock _ => ""
- | 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
- | Unparseable vs => #text vs
- | Metainfo vs => #text vs
- | _ => ""
-
-
- val unparse_doc = map unparse_elt
-
-
- (* Names of all PGIP document markup elements *)
- val doc_markup_elements =
- ["openblock",
- "closeblock",
- "opentheory",
- "theoryitem",
- "closetheory",
- "opengoal",
- "proofstep",
- "closegoal",
- "giveupgoal",
- "postponegoal",
- "comment",
- "doccomment",
- "whitespace",
- "spuriouscmd",
- "badcmd",
- (* the prover shouldn't really receive the next ones,
- but we include them here so that they are harmlessly
- ignored. *)
- "unparseable",
- "metainfo",
- (* Broker document format *)
- "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 Mon May 13 20:35:04 2013 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML Mon May 13 21:03:30 2013 +0200
@@ -6,326 +6,44 @@
signature PGIPOUTPUT =
sig
- (* These are the PGIP messages which the prover emits. *)
- datatype pgipoutput =
- Normalresponse of { content: XML.tree list }
- | Errorresponse of { fatality: PgipTypes.fatality,
- location: PgipTypes.location option,
- 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.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 }
- | Delids of { idtables: PgipTypes.idtable list }
- | Addids of { idtables: PgipTypes.idtable list }
- | Hasprefs of { prefcategory: string option,
+ datatype pgipoutput =
+ Hasprefs of { prefcategory: string option,
prefs: PgipTypes.preference list }
- | Prefval of { name: string, value: string }
- | Setrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option,
- idtables: PgipTypes.idtable list,
- fileurls : PgipTypes.pgipurl list }
- | Idvalue of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname,
- 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.tree list } (* errs to become PGML *)
- | Usespgip of { version: string,
- pgipelems: (string * bool * string list) list }
- | Usespgml of { version: string }
- | Pgip of { tag: string option,
- class: string,
- seq: int, id: string,
+ | Pgip of { tag: string option,
+ class: string,
+ seq: int, id: string,
destid: string option,
refid: string option,
refseq: int option,
content: XML.tree list }
- | Ready of { }
- val output : pgipoutput -> XML.tree
+ val output : pgipoutput -> XML.tree
end
structure PgipOutput : PGIPOUTPUT =
struct
-open PgipTypes
-datatype pgipoutput =
- Normalresponse of { content: XML.tree list }
- | Errorresponse of { fatality: fatality,
- location: location option,
- 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.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 }
- | Delids of { idtables: PgipTypes.idtable list }
- | Addids of { idtables: PgipTypes.idtable list }
- | Hasprefs of { prefcategory: string option, prefs: preference list }
- | Prefval of { name: string, value: string }
- | Idvalue of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname,
- text: XML.tree list }
- | Setrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option,
- idtables: PgipTypes.idtable list,
- fileurls : PgipTypes.pgipurl 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.tree list } (* errs to become PGML *)
- | Usespgip of { version: string,
- pgipelems: (string * bool * string list) list }
- | Usespgml of { version: string }
- | Pgip of { tag: string option,
- class: string,
- seq: int, id: string,
+datatype pgipoutput =
+ Hasprefs of { prefcategory: string option,
+ prefs: PgipTypes.preference list }
+ | Pgip of { tag: string option,
+ class: string,
+ seq: int, id: string,
destid: string option,
refid: string option,
refseq: int option,
content: XML.tree list }
- | Ready of { }
-
-(* Construct output XML messages *)
-
-fun normalresponse (Normalresponse vs) =
- let
- val content = #content vs
- in
- XML.Elem (("normalresponse", []), content)
- end
-
-fun errorresponse (Errorresponse vs) =
- let
- val fatality = #fatality vs
- val location = #location vs
- val content = #content vs
- in
- XML.Elem (("errorresponse",
- attrs_of_fatality fatality @
- these (Option.map attrs_of_location location)),
- content)
- end
-
-fun informfileloaded (Informfileloaded vs) =
- let
- val url = #url vs
- val completed = #completed vs
- in
- XML.Elem (("informfileloaded",
- attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed))),
- [])
- end
-
-fun informfileoutdated (Informfileoutdated vs) =
- let
- val url = #url vs
- val completed = #completed vs
- in
- XML.Elem (("informfileoutdated",
- attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed))),
- [])
- end
-
-fun informfileretracted (Informfileretracted vs) =
+fun output (Hasprefs vs) =
let
- val url = #url vs
- val completed = #completed vs
- in
- XML.Elem (("informfileretracted",
- attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed))),
- [])
- end
-
-fun metainforesponse (Metainforesponse vs) =
- let
- val attrs = #attrs vs
- val content = #content vs
- in
- XML.Elem (("metainforesponse", attrs), content)
- end
-
-fun lexicalstructure (Lexicalstructure vs) =
- let
- val content = #content vs
- in
- XML.Elem (("lexicalstructure", []), content)
+ val prefcategory = #prefcategory vs
+ val prefs = #prefs vs
+ in
+ XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory),
+ map PgipTypes.haspref prefs)
end
-
-fun proverinfo (Proverinfo vs) =
- let
- val name = #name vs
- val version = #version vs
- val instance = #instance vs
- val descr = #descr vs
- val url = #url vs
- val filenameextns = #filenameextns vs
- in
- XML.Elem (("proverinfo",
- [("name", name),
- ("version", version),
- ("instance", instance),
- ("descr", descr),
- ("url", Url.implode url),
- ("filenameextns", filenameextns)]),
- [])
- end
-
-fun setids (Setids vs) =
- let
- val idtables = #idtables vs
- in
- XML.Elem (("setids", []), map idtable_to_xml idtables)
- end
-
-fun setrefs (Setrefs vs) =
+ | output (Pgip vs) =
let
- val url = #url vs
- val thyname = #thyname vs
- val objtype = #objtype vs
- val name = #name vs
- val idtables = #idtables vs
- val fileurls = #fileurls vs
- fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
- in
- XML.Elem (("setrefs",
- (the_default [] (Option.map attrs_of_pgipurl url)) @
- (the_default [] (Option.map attrs_of_objtype objtype)) @
- (opt_attr "thyname" thyname) @
- (opt_attr "name" name)),
- (map idtable_to_xml idtables) @
- (map fileurl_to_xml fileurls))
- end
-
-fun addids (Addids vs) =
- let
- val idtables = #idtables vs
- in
- XML.Elem (("addids", []), map idtable_to_xml idtables)
- end
-
-fun delids (Delids vs) =
- let
- val idtables = #idtables vs
- in
- XML.Elem (("delids", []), map idtable_to_xml idtables)
- end
-
-fun hasprefs (Hasprefs vs) =
- let
- val prefcategory = #prefcategory vs
- val prefs = #prefs vs
- in
- XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
- end
-
-fun prefval (Prefval vs) =
- let
- val name = #name vs
- val value = #value vs
- in
- XML.Elem (("prefval", attr "name" name), [XML.Text value])
- end
-
-fun idvalue (Idvalue vs) =
- let
- val objtype_attrs = attrs_of_objtype (#objtype vs)
- val thyname = #thyname vs
- val name = #name vs
- val text = #text vs
- in
- XML.Elem (("idvalue",
- objtype_attrs @
- (opt_attr "thyname" thyname) @
- attr "name" name),
- text)
- end
-
-fun informguise (Informguise vs) =
- let
- val file = #file vs
- val theory = #theory vs
- val theorem = #theorem vs
- val proofpos = #proofpos vs
-
- fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
-
- val guisefile = elto "guisefile" attrs_of_pgipurl file
- val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
- val guiseproof = elto "guiseproof"
- (fn thm=>(attr "thmname" thm) @
- (opt_attr "proofpos" (Option.map string_of_int proofpos))) theorem
- in
- XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
- end
-
-fun parseresult (Parseresult vs) =
- let
- val attrs = #attrs vs
- val doc = #doc vs
- val errs = #errs vs
- val xmldoc = PgipMarkup.output_doc doc
- in
- XML.Elem (("parseresult", attrs), errs @ xmldoc)
- end
-
-fun acceptedpgipelems (Usespgip vs) =
- let
- val pgipelems = #pgipelems vs
- 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.Text e])
-
- in
- XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
- end
-
-fun usespgip (Usespgip vs) =
- let
- val version = #version vs
- val acceptedelems = acceptedpgipelems (Usespgip vs)
- in
- XML.Elem (("usespgip", attr "version" version), [acceptedelems])
- end
-
-fun usespgml (Usespgml vs) =
- let
- val version = #version vs
- in
- XML.Elem (("usespgml", attr "version" version), [])
- end
-
-fun pgip (Pgip vs) =
- let
val tag = #tag vs
val class = #class vs
val seq = #seq vs
@@ -336,41 +54,15 @@
val content = #content vs
in
XML.Elem(("pgip",
- opt_attr "tag" tag @
- attr "id" id @
- opt_attr "destid" destid @
- attr "class" class @
- opt_attr "refid" refid @
- opt_attr_map string_of_int "refseq" refseq @
- attr "seq" (string_of_int seq)),
+ PgipTypes.opt_attr "tag" tag @
+ PgipTypes.attr "id" id @
+ PgipTypes.opt_attr "destid" destid @
+ PgipTypes.attr "class" class @
+ PgipTypes.opt_attr "refid" refid @
+ PgipTypes.opt_attr_map string_of_int "refseq" refseq @
+ PgipTypes.attr "seq" (string_of_int seq)),
content)
end
-fun ready (Ready _) = XML.Elem (("ready", []), [])
-
-
-fun output pgipoutput = case pgipoutput of
- Normalresponse _ => normalresponse pgipoutput
- | Errorresponse _ => errorresponse pgipoutput
- | Informfileloaded _ => informfileloaded pgipoutput
- | Informfileoutdated _ => informfileoutdated pgipoutput
- | Informfileretracted _ => informfileretracted pgipoutput
- | Metainforesponse _ => metainforesponse pgipoutput
- | Lexicalstructure _ => lexicalstructure pgipoutput
- | Proverinfo _ => proverinfo pgipoutput
- | Setids _ => setids pgipoutput
- | Setrefs _ => setrefs pgipoutput
- | Addids _ => addids pgipoutput
- | Delids _ => delids pgipoutput
- | Hasprefs _ => hasprefs pgipoutput
- | Prefval _ => prefval pgipoutput
- | Idvalue _ => idvalue pgipoutput
- | Informguise _ => informguise pgipoutput
- | Parseresult _ => parseresult pgipoutput
- | Usespgip _ => usespgip pgipoutput
- | Usespgml _ => usespgml pgipoutput
- | Pgip _ => pgip pgipoutput
- | Ready _ => ready pgipoutput
-
end
--- a/src/Pure/ProofGeneral/pgip_parser.ML Mon May 13 20:35:04 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-(* Title: Pure/ProofGeneral/pgip_parser.ML
- Author: David Aspinall and Makarius
-
-Parsing theory sources without execution (via keyword classification).
-*)
-
-signature PGIP_PARSER =
-sig
- val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
-end
-
-structure PgipParser: PGIP_PARSER =
-struct
-
-structure D = PgipMarkup;
-structure I = PgipIsabelle;
-
-
-fun badcmd text = [D.Badcmd {text = text}];
-
-fun thy_begin text =
- (case try (Thy_Header.read Position.none) text of
- NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
- | SOME {name = (name, _), imports, ...} =>
- D.Opentheory {thyname = SOME name, parentnames = map #1 imports, text = text})
- :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
-
-fun thy_heading text =
- [D.Closeblock {},
- D.Doccomment {text = text},
- D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
-
-fun thy_decl text =
- [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
-
-fun goal text =
- [D.Opengoal {thmname = NONE, text = text},
- D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
-
-fun prf_block text =
- [D.Closeblock {},
- D.Proofstep {text = text},
- D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
-
-fun prf_open text =
- [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
- D.Proofstep {text = text}];
-
-fun proofstep text = [D.Proofstep {text = text}];
-fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
-
-
-fun command k f = Symtab.update_new (Keyword.kind_of k, f);
-
-val command_keywords = Symtab.empty
- |> command Keyword.control badcmd
- |> command Keyword.diag (fn text => [D.Spuriouscmd {text = text}])
- |> command Keyword.thy_begin thy_begin
- |> command Keyword.thy_end (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
- |> command Keyword.thy_heading1 thy_heading
- |> command Keyword.thy_heading2 thy_heading
- |> command Keyword.thy_heading3 thy_heading
- |> command Keyword.thy_heading4 thy_heading
- |> command Keyword.thy_load thy_decl
- |> command Keyword.thy_decl thy_decl
- |> command Keyword.thy_script thy_decl
- |> command Keyword.thy_goal goal
- |> command Keyword.qed closegoal
- |> command Keyword.qed_block closegoal
- |> command Keyword.qed_global (fn text => [D.Giveupgoal {text = text}])
- |> command Keyword.prf_heading2 (fn text => [D.Doccomment {text = text}])
- |> command Keyword.prf_heading3 (fn text => [D.Doccomment {text = text}])
- |> command Keyword.prf_heading4 (fn text => [D.Doccomment {text = text}])
- |> command Keyword.prf_goal goal
- |> command Keyword.prf_block prf_block
- |> command Keyword.prf_open prf_open
- |> command Keyword.prf_close (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
- |> command Keyword.prf_chain proofstep
- |> command Keyword.prf_decl proofstep
- |> command Keyword.prf_asm proofstep
- |> command Keyword.prf_asm_goal goal
- |> command Keyword.prf_script proofstep;
-
-val _ = subset (op =) (map Keyword.kind_of Keyword.kinds, Symtab.keys command_keywords)
- orelse raise Fail "Incomplete coverage of command keywords";
-
-fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
- | parse_command name text =
- (case Keyword.command_keyword name of
- NONE => [D.Unparseable {text = text}]
- | SOME k =>
- (case Symtab.lookup command_keywords (Keyword.kind_of k) of
- NONE => [D.Unparseable {text = text}]
- | SOME f => f text));
-
-fun parse_span span =
- let
- val kind = Thy_Syntax.span_kind span;
- val toks = Thy_Syntax.span_content span;
- val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
- in
- (case kind of
- Thy_Syntax.Command (name, _) => parse_command name text
- | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
- | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
- end;
-
-
-fun pgip_parser pos str =
- Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) pos str
- |> Thy_Syntax.parse_spans
- |> maps parse_span;
-
-end;
--- a/src/Pure/ProofGeneral/pgml.ML Mon May 13 20:35:04 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-(* Title: Pure/ProofGeneral/pgml.ML
- Author: David Aspinall
-
-PGIP abstraction: PGML
-*)
-
-signature PGML =
-sig
- type pgmlsym = { name: string, content: string }
-
- datatype pgmlatom = Sym of pgmlsym | Str of string
-
- datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
-
- datatype pgmlplace = Subscript | Superscript | Above | Below
-
- datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
-
- datatype pgmlaction = Toggle | Button | Menu
-
- datatype pgmlterm =
- Atoms of { kind: string option, content: pgmlatom list }
- | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
- | Break of { mandatory: bool option, indent: int option }
- | Subterm of { kind: string option,
- param: string option,
- place: pgmlplace option,
- name: string option,
- decoration: pgmldec option,
- action: pgmlaction option,
- pos: string option,
- xref: PgipTypes.pgipurl option,
- content: pgmlterm list }
- | Alt of { kind: string option, content: pgmlterm list }
- | Embed of XML.tree list
- | Raw of XML.tree
-
- datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
- content: pgmlterm list }
-
- val atom_to_xml : pgmlatom -> XML.tree
- val pgmlterm_to_xml : pgmlterm -> XML.tree
-
- val pgml_to_xml : pgml -> XML.tree
-end
-
-
-structure Pgml : PGML =
-struct
- open PgipTypes
-
- type pgmlsym = { name: string, content: string }
-
- datatype pgmlatom = Sym of pgmlsym | Str of string
-
- datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
-
- datatype pgmlplace = Subscript | Superscript | Above | Below
-
- datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
-
- datatype pgmlaction = Toggle | Button | Menu
-
- datatype pgmlterm =
- Atoms of { kind: string option, content: pgmlatom list }
- | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
- | Break of { mandatory: bool option, indent: int option }
- | Subterm of { kind: string option,
- param: string option,
- place: pgmlplace option,
- name: string option,
- decoration: pgmldec option,
- action: pgmlaction option,
- pos: string option,
- xref: PgipTypes.pgipurl option,
- content: pgmlterm list }
- | Alt of { kind: string option, content: pgmlterm list }
- | Embed of XML.tree list
- | Raw of XML.tree
-
-
- datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
- content: pgmlterm list }
-
- fun pgmlorient_to_string HOVOrient = "hov"
- | pgmlorient_to_string HOrient = "h"
- | pgmlorient_to_string VOrient = "v"
- | pgmlorient_to_string HVOrient = "hv"
-
- fun pgmlplace_to_string Subscript = "sub"
- | pgmlplace_to_string Superscript = "sup"
- | pgmlplace_to_string Above = "above"
- | pgmlplace_to_string Below = "below"
-
- fun pgmldec_to_string Bold = "bold"
- | pgmldec_to_string Italic = "italic"
- | pgmldec_to_string Error = "error"
- | pgmldec_to_string Warning = "warning"
- | pgmldec_to_string Info = "info"
- | pgmldec_to_string (Other s) = "other"
-
- fun pgmlaction_to_string Toggle = "toggle"
- | pgmlaction_to_string Button = "button"
- | pgmlaction_to_string Menu = "menu"
-
- (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
- would be better not to *) (* FIXME !??? *)
- fun atom_to_xml (Sym {name, content}) = XML.Elem (("sym", attr "name" name), [XML.Text content])
- | atom_to_xml (Str content) = XML.Text content;
-
- fun pgmlterm_to_xml (Atoms {kind, content}) =
- XML.Elem(("atom", opt_attr "kind" kind), map atom_to_xml content)
-
- | pgmlterm_to_xml (Box {orient, indent, content}) =
- XML.Elem(("box",
- opt_attr_map pgmlorient_to_string "orient" orient @
- opt_attr_map int_to_pgstring "indent" indent),
- map pgmlterm_to_xml content)
-
- | pgmlterm_to_xml (Break {mandatory, indent}) =
- XML.Elem(("break",
- opt_attr_map bool_to_pgstring "mandatory" mandatory @
- opt_attr_map int_to_pgstring "indent" indent), [])
-
- | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
- XML.Elem(("subterm",
- opt_attr "kind" kind @
- opt_attr "param" param @
- opt_attr_map pgmlplace_to_string "place" place @
- opt_attr "name" name @
- opt_attr_map pgmldec_to_string "decoration" decoration @
- opt_attr_map pgmlaction_to_string "action" action @
- opt_attr "pos" pos @
- opt_attr_map string_of_pgipurl "xref" xref),
- map pgmlterm_to_xml content)
-
- | pgmlterm_to_xml (Alt {kind, content}) =
- XML.Elem(("alt", opt_attr "kind" kind), map pgmlterm_to_xml content)
-
- | pgmlterm_to_xml (Embed xmls) = XML.Elem(("embed", []), xmls)
-
- | pgmlterm_to_xml (Raw xml) = xml
-
-
- datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
- content: pgmlterm list }
-
- fun pgml_to_xml (Pgml {version,systemid,area,content}) =
- XML.Elem(("pgml",
- opt_attr "version" version @
- opt_attr "systemid" systemid @
- the_default [] (Option.map PgipTypes.attrs_of_displayarea area)),
- map pgmlterm_to_xml content)
-end
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 20:35:04 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 21:03:30 2013 +0200
@@ -17,12 +17,6 @@
structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
struct
-open PgipTypes;
-open PgipMarkup;
-open PgipInput;
-open PgipOutput;
-
-
(** print mode **)
val proof_general_emacsN = "ProofGeneralEmacs";
@@ -41,7 +35,7 @@
fun pgip_serial () = Unsynchronized.inc pgip_seq
fun assemble_pgips pgips =
- Pgip { tag = SOME pgip_tag,
+ PgipOutput.Pgip { tag = SOME pgip_tag,
class = pgip_class,
seq = pgip_serial (),
id = pgip_id,
@@ -110,7 +104,7 @@
local
-fun invalid_pgip () = raise PGIP "Invalid PGIP packet received";
+fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
fun output_emacs pgips = Output.urgent_message (output_pgips pgips);
@@ -120,7 +114,8 @@
{name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
in
! preferences |> List.app (fn (prefcat, prefs) =>
- output_emacs [Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
+ output_emacs
+ [PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
end
| process_element_emacs (XML.Elem (("setpref", attrs), data)) =
let
@@ -157,7 +152,7 @@
else ()
end
| _ => invalid_pgip ())
- end handle PGIP msg => error (msg ^ "\n" ^ str);
+ end handle PgipTypes.PGIP msg => error (msg ^ "\n" ^ str);
val _ =
Outer_Syntax.improper_command
--- a/src/Pure/ROOT Mon May 13 20:35:04 2013 +0200
+++ b/src/Pure/ROOT Mon May 13 21:03:30 2013 +0200
@@ -160,13 +160,8 @@
"Proof/proof_rewrite_rules.ML"
"Proof/proof_syntax.ML"
"Proof/reconstruct.ML"
- "ProofGeneral/pgip_input.ML"
- "ProofGeneral/pgip_isabelle.ML"
- "ProofGeneral/pgip_markup.ML"
"ProofGeneral/pgip_output.ML"
- "ProofGeneral/pgip_parser.ML"
"ProofGeneral/pgip_types.ML"
- "ProofGeneral/pgml.ML"
"ProofGeneral/preferences.ML"
"ProofGeneral/proof_general_emacs.ML"
"ProofGeneral/proof_general_pgip.ML"
--- a/src/Pure/ROOT.ML Mon May 13 20:35:04 2013 +0200
+++ b/src/Pure/ROOT.ML Mon May 13 21:03:30 2013 +0200
@@ -299,20 +299,13 @@
(* configuration for Proof General *)
use "ProofGeneral/pgip_types.ML";
-use "ProofGeneral/pgml.ML";
-use "ProofGeneral/pgip_markup.ML";
-use "ProofGeneral/pgip_input.ML";
use "ProofGeneral/pgip_output.ML";
-use "ProofGeneral/pgip_isabelle.ML";
-
(use
|> Unsynchronized.setmp Proofterm.proofs 0
|> Unsynchronized.setmp Multithreading.max_threads 0)
"ProofGeneral/preferences.ML";
-use "ProofGeneral/pgip_parser.ML";
-
use "ProofGeneral/proof_general_pgip.ML";
use "ProofGeneral/proof_general_emacs.ML";