# HG changeset patch # User wenzelm # Date 1368471810 -7200 # Node ID 43fbd02eb9d0d760ef40aa3f7282418efb91ca46 # Parent 0e18eee8c2c274591330c4aac0870df03d74db03 removed obsolete PGIP material; diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/pgip_input.ML --- 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 diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/pgip_isabelle.ML --- 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 diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/pgip_markup.ML --- 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; diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/pgip_output.ML --- 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 diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/pgip_parser.ML --- 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; diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/pgml.ML --- 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 diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ROOT --- 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" diff -r 0e18eee8c2c2 -r 43fbd02eb9d0 src/Pure/ROOT.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";