1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML Mon May 13 20:35:04 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,239 +0,0 @@
1.4 -(* Title: Pure/ProofGeneral/pgip_input.ML
1.5 - Author: David Aspinall
1.6 -
1.7 -PGIP abstraction: input commands.
1.8 -*)
1.9 -
1.10 -signature PGIPINPUT =
1.11 -sig
1.12 - (* These are the PGIP commands to which we respond. *)
1.13 - datatype pgipinput =
1.14 - (* protocol/prover config *)
1.15 - Askpgip of { }
1.16 - | Askpgml of { }
1.17 - | Askconfig of { }
1.18 - | Askprefs of { }
1.19 - | Setpref of { name:string, prefcategory:string option, value:string }
1.20 - | Getpref of { name:string, prefcategory:string option }
1.21 - (* prover control *)
1.22 - | Proverinit of { }
1.23 - | Proverexit of { }
1.24 - | Setproverflag of { flagname:string, value: bool }
1.25 - (* improper proof commands: control proof state *)
1.26 - | Dostep of { text: string }
1.27 - | Undostep of { times: int }
1.28 - | Redostep of { }
1.29 - | Abortgoal of { }
1.30 - | Forget of { thyname: string option, name: string option,
1.31 - objtype: PgipTypes.objtype option }
1.32 - | Restoregoal of { thmname : string }
1.33 - (* context inspection commands *)
1.34 - | Askids of { url: PgipTypes.pgipurl option,
1.35 - thyname: PgipTypes.objname option,
1.36 - objtype: PgipTypes.objtype option }
1.37 - | Askrefs of { url: PgipTypes.pgipurl option,
1.38 - thyname: PgipTypes.objname option,
1.39 - objtype: PgipTypes.objtype option,
1.40 - name: PgipTypes.objname option }
1.41 - | Showid of { thyname: PgipTypes.objname option,
1.42 - objtype: PgipTypes.objtype,
1.43 - name: PgipTypes.objname }
1.44 - | Askguise of { }
1.45 - | Parsescript of { text: string, location: PgipTypes.location,
1.46 - systemdata: string option }
1.47 - | Showproofstate of { }
1.48 - | Showctxt of { }
1.49 - | Searchtheorems of { arg: string }
1.50 - | Setlinewidth of { width: int }
1.51 - | Viewdoc of { arg: string }
1.52 - (* improper theory-level commands *)
1.53 - | Doitem of { text: string }
1.54 - | Undoitem of { }
1.55 - | Redoitem of { }
1.56 - | Aborttheory of { }
1.57 - | Retracttheory of { thyname: string }
1.58 - | Loadfile of { url: PgipTypes.pgipurl }
1.59 - | Openfile of { url: PgipTypes.pgipurl }
1.60 - | Closefile of { }
1.61 - | Abortfile of { }
1.62 - | Retractfile of { url: PgipTypes.pgipurl }
1.63 - | Changecwd of { url: PgipTypes.pgipurl }
1.64 - | Systemcmd of { arg: string }
1.65 - (* unofficial escape command for debugging *)
1.66 - | Quitpgip of { }
1.67 -
1.68 - val input: Markup.T * XML.tree list -> pgipinput option (* raises PGIP *)
1.69 -end
1.70 -
1.71 -structure PgipInput : PGIPINPUT =
1.72 -struct
1.73 -
1.74 -open PgipTypes
1.75 -
1.76 -(*** PGIP input ***)
1.77 -
1.78 -datatype pgipinput =
1.79 - (* protocol/prover config *)
1.80 - Askpgip of { }
1.81 - | Askpgml of { }
1.82 - | Askconfig of { }
1.83 - | Askprefs of { }
1.84 - | Setpref of { name:string, prefcategory:string option, value:string }
1.85 - | Getpref of { name:string, prefcategory:string option }
1.86 - (* prover control *)
1.87 - | Proverinit of { }
1.88 - | Proverexit of { }
1.89 - | Setproverflag of { flagname:string, value: bool }
1.90 - (* improper proof commands: control proof state *)
1.91 - | Dostep of { text: string }
1.92 - | Undostep of { times: int }
1.93 - | Redostep of { }
1.94 - | Abortgoal of { }
1.95 - | Forget of { thyname: string option, name: string option,
1.96 - objtype: PgipTypes.objtype option }
1.97 - | Restoregoal of { thmname : string }
1.98 - (* context inspection commands *)
1.99 - | Askids of { url: PgipTypes.pgipurl option,
1.100 - thyname: PgipTypes.objname option,
1.101 - objtype: PgipTypes.objtype option }
1.102 - | Askrefs of { url: PgipTypes.pgipurl option,
1.103 - thyname: PgipTypes.objname option,
1.104 - objtype: PgipTypes.objtype option,
1.105 - name: PgipTypes.objname option }
1.106 - | Showid of { thyname: PgipTypes.objname option,
1.107 - objtype: PgipTypes.objtype,
1.108 - name: PgipTypes.objname }
1.109 - | Askguise of { }
1.110 - | Parsescript of { text: string, location: location,
1.111 - systemdata: string option }
1.112 - | Showproofstate of { }
1.113 - | Showctxt of { }
1.114 - | Searchtheorems of { arg: string }
1.115 - | Setlinewidth of { width: int }
1.116 - | Viewdoc of { arg: string }
1.117 - (* improper theory-level commands *)
1.118 - | Doitem of { text: string }
1.119 - | Undoitem of { }
1.120 - | Redoitem of { }
1.121 - | Aborttheory of { }
1.122 - | Retracttheory of { thyname: string }
1.123 - | Loadfile of { url: pgipurl }
1.124 - | Openfile of { url: pgipurl }
1.125 - | Closefile of { }
1.126 - | Abortfile of { }
1.127 - | Retractfile of { url: pgipurl }
1.128 - | Changecwd of { url: pgipurl }
1.129 - | Systemcmd of { arg: string }
1.130 - (* unofficial escape command for debugging *)
1.131 - | Quitpgip of { }
1.132 -
1.133 -(* Extracting content from input XML elements to make a PGIPinput *)
1.134 -local
1.135 -
1.136 - val thyname_attro = get_attr_opt "thyname"
1.137 - val thyname_attr = get_attr "thyname"
1.138 - val name_attr = get_attr "name"
1.139 - val name_attro = get_attr_opt "name"
1.140 - val thmname_attr = get_attr "thmname"
1.141 - val flagname_attr = get_attr "flagname"
1.142 - val value_attr = get_attr "value"
1.143 -
1.144 - fun objtype_attro attrs = if has_attr "objtype" attrs then
1.145 - SOME (objtype_of_attrs attrs)
1.146 - else NONE
1.147 -
1.148 - fun pgipurl_attro attrs = if has_attr "url" attrs then
1.149 - SOME (pgipurl_of_attrs attrs)
1.150 - else NONE
1.151 -
1.152 - val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
1.153 - val prefcat_attr = get_attr_opt "prefcategory"
1.154 -
1.155 - fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
1.156 - | xmltext [] = ""
1.157 - | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
1.158 -
1.159 - exception Unknown
1.160 - exception NoAction
1.161 -in
1.162 -
1.163 -(* Return a valid PGIP input command.
1.164 - Raise PGIP exception for invalid data.
1.165 - Return NONE for unknown/unhandled commands.
1.166 -*)
1.167 -fun input ((elem, attrs), data) =
1.168 -SOME
1.169 - (case elem of
1.170 - "askpgip" => Askpgip { }
1.171 - | "askpgml" => Askpgml { }
1.172 - | "askconfig" => Askconfig { }
1.173 - (* proverconfig *)
1.174 - | "askprefs" => Askprefs { }
1.175 - | "getpref" => Getpref { name = name_attr attrs,
1.176 - prefcategory = prefcat_attr attrs }
1.177 - | "setpref" => Setpref { name = name_attr attrs,
1.178 - prefcategory = prefcat_attr attrs,
1.179 - value = xmltext data }
1.180 - (* provercontrol *)
1.181 - | "proverinit" => Proverinit { }
1.182 - | "proverexit" => Proverexit { }
1.183 - | "setproverflag" => Setproverflag { flagname = flagname_attr attrs,
1.184 - value = read_pgipbool (value_attr attrs) }
1.185 - (* improperproofcmd: improper commands not in script *)
1.186 - | "dostep" => Dostep { text = xmltext data }
1.187 - | "undostep" => Undostep { times = times_attr attrs }
1.188 - | "redostep" => Redostep { }
1.189 - | "abortgoal" => Abortgoal { }
1.190 - | "forget" => Forget { thyname = thyname_attro attrs,
1.191 - name = name_attro attrs,
1.192 - objtype = objtype_attro attrs }
1.193 - | "restoregoal" => Restoregoal { thmname = thmname_attr attrs}
1.194 - (* proofctxt: improper commands *)
1.195 - | "askids" => Askids { url = pgipurl_attro attrs,
1.196 - thyname = thyname_attro attrs,
1.197 - objtype = objtype_attro attrs }
1.198 - | "askrefs" => Askrefs { url = pgipurl_attro attrs,
1.199 - thyname = thyname_attro attrs,
1.200 - objtype = objtype_attro attrs,
1.201 - name = name_attro attrs }
1.202 - | "showid" => Showid { thyname = thyname_attro attrs,
1.203 - objtype = objtype_of_attrs attrs,
1.204 - name = name_attr attrs }
1.205 - | "askguise" => Askguise { }
1.206 - | "parsescript" => Parsescript { text = (xmltext data),
1.207 - systemdata = get_attr_opt "systemdata" attrs,
1.208 - location = location_of_attrs attrs }
1.209 - | "showproofstate" => Showproofstate { }
1.210 - | "showctxt" => Showctxt { }
1.211 - | "searchtheorems" => Searchtheorems { arg = xmltext data }
1.212 - | "setlinewidth" => Setlinewidth { width = read_pgipnat (xmltext data) }
1.213 - | "viewdoc" => Viewdoc { arg = xmltext data }
1.214 - (* improperfilecmd: theory-level commands not in script *)
1.215 - | "doitem" => Doitem { text = xmltext data }
1.216 - | "undoitem" => Undoitem { }
1.217 - | "redoitem" => Redoitem { }
1.218 - | "aborttheory" => Aborttheory { }
1.219 - | "retracttheory" => Retracttheory { thyname = thyname_attr attrs }
1.220 - | "loadfile" => Loadfile { url = pgipurl_of_attrs attrs }
1.221 - | "openfile" => Openfile { url = pgipurl_of_attrs attrs }
1.222 - | "closefile" => Closefile { }
1.223 - | "abortfile" => Abortfile { }
1.224 - | "retractfile" => Retractfile { url = pgipurl_of_attrs attrs }
1.225 - | "changecwd" => Changecwd { url = pgipurl_of_attrs attrs }
1.226 - | "systemcmd" => Systemcmd { arg = xmltext data }
1.227 - (* unofficial command for debugging *)
1.228 - | "quitpgip" => Quitpgip { }
1.229 -
1.230 - (* We allow sending proper document markup too; we map it back to dostep *)
1.231 - (* and strip out metainfo elements. Markup correctness isn't checked: this *)
1.232 - (* is a compatibility measure to make it easy for interfaces. *)
1.233 - | x => if member (op =) PgipMarkup.doc_markup_elements x then
1.234 - if member (op =) PgipMarkup.doc_markup_elements_ignored x then
1.235 - raise NoAction
1.236 - else
1.237 - Dostep { text = xmltext data } (* could separate out Doitem too *)
1.238 - else raise Unknown)
1.239 - handle Unknown => NONE | NoAction => NONE
1.240 -end
1.241 -
1.242 -end
2.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML Mon May 13 20:35:04 2013 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,111 +0,0 @@
2.4 -(* Title: Pure/ProofGeneral/pgip_isabelle.ML
2.5 - Author: David Aspinall
2.6 -
2.7 -Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
2.8 -*)
2.9 -
2.10 -signature PGIP_ISABELLE =
2.11 -sig
2.12 - val isabelle_pgml_version_supported : string
2.13 - val isabelle_pgip_version_supported : string
2.14 - val systemid : string
2.15 - val accepted_inputs : (string * bool * (string list)) list
2.16 -
2.17 - val location_of_position : Position.T -> PgipTypes.location
2.18 -
2.19 - (* Additional types of objects in Isar scripts *)
2.20 -
2.21 - val ObjTheoryBody : PgipTypes.objtype
2.22 - val ObjTheoryDecl : PgipTypes.objtype
2.23 - val ObjTheoryBodySubsection : PgipTypes.objtype
2.24 - val ObjProofBody : PgipTypes.objtype
2.25 - val ObjFormalComment : PgipTypes.objtype
2.26 - val ObjClass : PgipTypes.objtype
2.27 - val ObjTheoremSet : PgipTypes.objtype
2.28 - val ObjOracle : PgipTypes.objtype
2.29 - val ObjLocale : PgipTypes.objtype
2.30 -
2.31 -end
2.32 -
2.33 -structure PgipIsabelle : PGIP_ISABELLE =
2.34 -struct
2.35 -
2.36 -val isabelle_pgml_version_supported = "2.0";
2.37 -val isabelle_pgip_version_supported = "2.0"
2.38 -val systemid = "Isabelle"
2.39 -
2.40 -
2.41 -(** Accepted commands **)
2.42 -
2.43 -local
2.44 -
2.45 - (* These element names are a subset of those in pgip_input.ML.
2.46 - They must be handled in proof_general_pgip.ML/process_pgip_element. *)
2.47 -
2.48 - val accepted_names =
2.49 - (* not implemented: "askconfig", "forget", "restoregoal" *)
2.50 - ["askpgip","askpgml","askprefs","getpref","setpref",
2.51 - "proverinit","proverexit","startquiet","stopquiet",
2.52 - "pgmlsymbolson", "pgmlsymbolsoff",
2.53 - "dostep", "undostep", "redostep", "abortgoal",
2.54 - "askids", "showid", "askguise",
2.55 - "parsescript",
2.56 - "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
2.57 - "doitem", "undoitem", "redoitem", "abortheory",
2.58 - "retracttheory", "loadfile", "openfile", "closefile",
2.59 - "abortfile", "retractfile", "changecwd", "systemcmd"];
2.60 -
2.61 - fun element_async p =
2.62 - false (* single threaded only *)
2.63 -
2.64 - fun supported_optional_attrs p = (case p of
2.65 - "undostep" => ["times"]
2.66 - (* TODO: we could probably extend these too:
2.67 - | "redostep" => ["times"]
2.68 - | "undoitem" => ["times"]
2.69 - | "redoitem" => ["times"] *)
2.70 - | _ => [])
2.71 -in
2.72 -val accepted_inputs =
2.73 - (map (fn p=> (p, element_async p, supported_optional_attrs p))
2.74 - accepted_names);
2.75 -end
2.76 -
2.77 -
2.78 -fun location_of_position pos =
2.79 - let val line = Position.line_of pos
2.80 - val (url,descr) =
2.81 - (case Position.file_of pos of
2.82 - NONE => (NONE, NONE)
2.83 - | SOME fname =>
2.84 - let val path = Path.explode fname in
2.85 - if File.exists path
2.86 - then (SOME (PgipTypes.pgipurl_of_path path), NONE)
2.87 - else (NONE, SOME fname)
2.88 - end);
2.89 - in
2.90 - { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
2.91 - end
2.92 -
2.93 -
2.94 -val [ObjTheoryBody,
2.95 - ObjTheoryDecl,
2.96 - ObjTheoryBodySubsection,
2.97 - ObjProofBody,
2.98 - ObjFormalComment,
2.99 - ObjClass,
2.100 - ObjTheoremSet,
2.101 - ObjOracle,
2.102 - ObjLocale] =
2.103 - map PgipTypes.ObjOther
2.104 - ["theory body",
2.105 - "theory declaration",
2.106 - "theory subsection",
2.107 - "proof body",
2.108 - "formal comment",
2.109 - "class",
2.110 - "theorem set declaration",
2.111 - "oracle",
2.112 - "locale"];
2.113 -
2.114 -end
3.1 --- a/src/Pure/ProofGeneral/pgip_markup.ML Mon May 13 20:35:04 2013 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,213 +0,0 @@
3.4 -(* Title: Pure/ProofGeneral/pgip_markup.ML
3.5 - Author: David Aspinall
3.6 -
3.7 -PGIP abstraction: document markup for proof scripts (in progress).
3.8 -*)
3.9 -
3.10 -signature PGIPMARKUP =
3.11 -sig
3.12 - (* Generic markup on sequential, non-overlapping pieces of proof text *)
3.13 - datatype pgipdoc =
3.14 - Openblock of { metavarid: string option, name: string option,
3.15 - objtype: PgipTypes.objtype option }
3.16 - | Closeblock of { }
3.17 - | Opentheory of { thyname: string option, parentnames: string list , text: string}
3.18 - | Theoryitem of { name: string option, objtype: PgipTypes.objtype option, text: string }
3.19 - | Closetheory of { text: string }
3.20 - | Opengoal of { thmname: string option, text: string }
3.21 - | Proofstep of { text: string }
3.22 - | Closegoal of { text: string }
3.23 - | Giveupgoal of { text: string }
3.24 - | Postponegoal of { text: string }
3.25 - | Comment of { text: string }
3.26 - | Doccomment of { text: string }
3.27 - | Whitespace of { text: string }
3.28 - | Spuriouscmd of { text: string }
3.29 - | Badcmd of { text: string }
3.30 - | Unparseable of { text: string }
3.31 - | Metainfo of { name: string option, text: string }
3.32 - (* Last three for PGIP literate markup only: *)
3.33 - | Litcomment of { format: string option, content: XML.tree list }
3.34 - | Showcode of { show: bool }
3.35 - | Setformat of { format: string }
3.36 -
3.37 - type pgipdocument = pgipdoc list
3.38 - type pgip_parser = string -> pgipdocument (* system must provide a parser P *)
3.39 - val unparse_doc : pgipdocument -> string list (* s.t. unparse (P x) = x *)
3.40 - val output_doc : pgipdocument -> XML.tree list
3.41 - val doc_markup_elements : string list (* used in pgip_input *)
3.42 - val doc_markup_elements_ignored : string list (* used in pgip_input *)
3.43 -end
3.44 -
3.45 -
3.46 -structure PgipMarkup : PGIPMARKUP =
3.47 -struct
3.48 - open PgipTypes
3.49 -
3.50 -(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
3.51 - datatype pgipdoc =
3.52 - Openblock of { metavarid: string option, name: string option,
3.53 - objtype: PgipTypes.objtype option }
3.54 - | Closeblock of { }
3.55 - | Opentheory of { thyname: string option, parentnames: string list, text: string}
3.56 - | Theoryitem of { name: string option, objtype: PgipTypes.objtype option, text: string }
3.57 - | Closetheory of { text: string }
3.58 - | Opengoal of { thmname: string option, text: string }
3.59 - | Proofstep of { text: string }
3.60 - | Closegoal of { text: string }
3.61 - | Giveupgoal of { text: string }
3.62 - | Postponegoal of { text: string }
3.63 - | Comment of { text: string }
3.64 - | Doccomment of { text: string }
3.65 - | Whitespace of { text: string }
3.66 - | Spuriouscmd of { text: string }
3.67 - | Badcmd of { text: string }
3.68 - | Unparseable of { text: string }
3.69 - | Metainfo of { name: string option, text: string }
3.70 - | Litcomment of { format: string option, content: XML.tree list }
3.71 - | Showcode of { show: bool }
3.72 - | Setformat of { format: string }
3.73 -
3.74 - type pgipdocument = pgipdoc list
3.75 - type pgip_parser = string -> pgipdocument
3.76 -
3.77 - fun xml_of docelt =
3.78 - case docelt of
3.79 -
3.80 - Openblock vs =>
3.81 - XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
3.82 - opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
3.83 - opt_attr "metavarid" (#metavarid vs)),
3.84 - [])
3.85 -
3.86 - | Closeblock _ =>
3.87 - XML.Elem(("closeblock", []), [])
3.88 -
3.89 - | Opentheory vs =>
3.90 - XML.Elem(("opentheory",
3.91 - opt_attr "thyname" (#thyname vs) @
3.92 - opt_attr "parentnames"
3.93 - (case (#parentnames vs)
3.94 - of [] => NONE
3.95 - | ps => SOME (space_implode ";" ps))),
3.96 - [XML.Text (#text vs)])
3.97 -
3.98 - | Theoryitem vs =>
3.99 - XML.Elem(("theoryitem",
3.100 - opt_attr "name" (#name vs) @
3.101 - opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs)),
3.102 - [XML.Text (#text vs)])
3.103 -
3.104 - | Closetheory vs =>
3.105 - XML.Elem(("closetheory", []), [XML.Text (#text vs)])
3.106 -
3.107 - | Opengoal vs =>
3.108 - XML.Elem(("opengoal",
3.109 - opt_attr "thmname" (#thmname vs)),
3.110 - [XML.Text (#text vs)])
3.111 -
3.112 - | Proofstep vs =>
3.113 - XML.Elem(("proofstep", []), [XML.Text (#text vs)])
3.114 -
3.115 - | Closegoal vs =>
3.116 - XML.Elem(("closegoal", []), [XML.Text (#text vs)])
3.117 -
3.118 - | Giveupgoal vs =>
3.119 - XML.Elem(("giveupgoal", []), [XML.Text (#text vs)])
3.120 -
3.121 - | Postponegoal vs =>
3.122 - XML.Elem(("postponegoal", []), [XML.Text (#text vs)])
3.123 -
3.124 - | Comment vs =>
3.125 - XML.Elem(("comment", []), [XML.Text (#text vs)])
3.126 -
3.127 - | Whitespace vs =>
3.128 - XML.Elem(("whitespace", []), [XML.Text (#text vs)])
3.129 -
3.130 - | Doccomment vs =>
3.131 - XML.Elem(("doccomment", []), [XML.Text (#text vs)])
3.132 -
3.133 - | Spuriouscmd vs =>
3.134 - XML.Elem(("spuriouscmd", []), [XML.Text (#text vs)])
3.135 -
3.136 - | Badcmd vs =>
3.137 - XML.Elem(("badcmd", []), [XML.Text (#text vs)])
3.138 -
3.139 - | Unparseable vs =>
3.140 - XML.Elem(("unparseable", []), [XML.Text (#text vs)])
3.141 -
3.142 - | Metainfo vs =>
3.143 - XML.Elem(("metainfo", opt_attr "name" (#name vs)),
3.144 - [XML.Text (#text vs)])
3.145 -
3.146 - | Litcomment vs =>
3.147 - XML.Elem(("litcomment", opt_attr "format" (#format vs)),
3.148 - #content vs)
3.149 -
3.150 - | Showcode vs =>
3.151 - XML.Elem(("showcode",
3.152 - attr "show" (PgipTypes.bool_to_pgstring (#show vs))), [])
3.153 -
3.154 - | Setformat vs =>
3.155 - XML.Elem(("setformat", attr "format" (#format vs)), [])
3.156 -
3.157 - val output_doc = map xml_of
3.158 -
3.159 - fun unparse_elt docelt =
3.160 - case docelt of
3.161 - Openblock _ => ""
3.162 - | Closeblock _ => ""
3.163 - | Opentheory vs => #text vs
3.164 - | Theoryitem vs => #text vs
3.165 - | Closetheory vs => #text vs
3.166 - | Opengoal vs => #text vs
3.167 - | Proofstep vs => #text vs
3.168 - | Closegoal vs => #text vs
3.169 - | Giveupgoal vs => #text vs
3.170 - | Postponegoal vs => #text vs
3.171 - | Comment vs => #text vs
3.172 - | Doccomment vs => #text vs
3.173 - | Whitespace vs => #text vs
3.174 - | Spuriouscmd vs => #text vs
3.175 - | Badcmd vs => #text vs
3.176 - | Unparseable vs => #text vs
3.177 - | Metainfo vs => #text vs
3.178 - | _ => ""
3.179 -
3.180 -
3.181 - val unparse_doc = map unparse_elt
3.182 -
3.183 -
3.184 - (* Names of all PGIP document markup elements *)
3.185 - val doc_markup_elements =
3.186 - ["openblock",
3.187 - "closeblock",
3.188 - "opentheory",
3.189 - "theoryitem",
3.190 - "closetheory",
3.191 - "opengoal",
3.192 - "proofstep",
3.193 - "closegoal",
3.194 - "giveupgoal",
3.195 - "postponegoal",
3.196 - "comment",
3.197 - "doccomment",
3.198 - "whitespace",
3.199 - "spuriouscmd",
3.200 - "badcmd",
3.201 - (* the prover shouldn't really receive the next ones,
3.202 - but we include them here so that they are harmlessly
3.203 - ignored. *)
3.204 - "unparseable",
3.205 - "metainfo",
3.206 - (* Broker document format *)
3.207 - "litcomment",
3.208 - "showcode",
3.209 - "setformat"]
3.210 -
3.211 - (* non-document/empty text, must be ignored *)
3.212 - val doc_markup_elements_ignored =
3.213 - [ "metainfo", "openblock", "closeblock",
3.214 - "litcomment", "showcode", "setformat" ]
3.215 -
3.216 -end;
4.1 --- a/src/Pure/ProofGeneral/pgip_output.ML Mon May 13 20:35:04 2013 +0200
4.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML Mon May 13 21:03:30 2013 +0200
4.3 @@ -6,326 +6,44 @@
4.4
4.5 signature PGIPOUTPUT =
4.6 sig
4.7 - (* These are the PGIP messages which the prover emits. *)
4.8 - datatype pgipoutput =
4.9 - Normalresponse of { content: XML.tree list }
4.10 - | Errorresponse of { fatality: PgipTypes.fatality,
4.11 - location: PgipTypes.location option,
4.12 - content: XML.tree list }
4.13 - | Informfileloaded of { url: PgipTypes.pgipurl, completed: bool }
4.14 - | Informfileoutdated of { url: PgipTypes.pgipurl, completed: bool }
4.15 - | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
4.16 - | Metainforesponse of { attrs: XML.attributes,
4.17 - content: XML.tree list }
4.18 - | Lexicalstructure of { content: XML.tree list }
4.19 - | Proverinfo of { name: string,
4.20 - version: string,
4.21 - instance: string,
4.22 - descr: string,
4.23 - url: Url.T,
4.24 - filenameextns: string }
4.25 - | Setids of { idtables: PgipTypes.idtable list }
4.26 - | Delids of { idtables: PgipTypes.idtable list }
4.27 - | Addids of { idtables: PgipTypes.idtable list }
4.28 - | Hasprefs of { prefcategory: string option,
4.29 + datatype pgipoutput =
4.30 + Hasprefs of { prefcategory: string option,
4.31 prefs: PgipTypes.preference list }
4.32 - | Prefval of { name: string, value: string }
4.33 - | Setrefs of { url: PgipTypes.pgipurl option,
4.34 - thyname: PgipTypes.objname option,
4.35 - objtype: PgipTypes.objtype option,
4.36 - name: PgipTypes.objname option,
4.37 - idtables: PgipTypes.idtable list,
4.38 - fileurls : PgipTypes.pgipurl list }
4.39 - | Idvalue of { thyname: PgipTypes.objname option,
4.40 - objtype: PgipTypes.objtype,
4.41 - name: PgipTypes.objname,
4.42 - text: XML.tree list }
4.43 - | Informguise of { file : PgipTypes.pgipurl option,
4.44 - theory: PgipTypes.objname option,
4.45 - theorem: PgipTypes.objname option,
4.46 - proofpos: int option }
4.47 - | Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument,
4.48 - errs: XML.tree list } (* errs to become PGML *)
4.49 - | Usespgip of { version: string,
4.50 - pgipelems: (string * bool * string list) list }
4.51 - | Usespgml of { version: string }
4.52 - | Pgip of { tag: string option,
4.53 - class: string,
4.54 - seq: int, id: string,
4.55 + | Pgip of { tag: string option,
4.56 + class: string,
4.57 + seq: int, id: string,
4.58 destid: string option,
4.59 refid: string option,
4.60 refseq: int option,
4.61 content: XML.tree list }
4.62 - | Ready of { }
4.63
4.64 - val output : pgipoutput -> XML.tree
4.65 + val output : pgipoutput -> XML.tree
4.66 end
4.67
4.68 structure PgipOutput : PGIPOUTPUT =
4.69 struct
4.70 -open PgipTypes
4.71
4.72 -datatype pgipoutput =
4.73 - Normalresponse of { content: XML.tree list }
4.74 - | Errorresponse of { fatality: fatality,
4.75 - location: location option,
4.76 - content: XML.tree list }
4.77 - | Informfileloaded of { url: Path.T, completed: bool }
4.78 - | Informfileoutdated of { url: Path.T, completed: bool }
4.79 - | Informfileretracted of { url: Path.T, completed: bool }
4.80 - | Metainforesponse of { attrs: XML.attributes, content: XML.tree list }
4.81 - | Lexicalstructure of { content: XML.tree list }
4.82 - | Proverinfo of { name: string, version: string, instance: string,
4.83 - descr: string, url: Url.T, filenameextns: string }
4.84 - | Setids of { idtables: PgipTypes.idtable list }
4.85 - | Delids of { idtables: PgipTypes.idtable list }
4.86 - | Addids of { idtables: PgipTypes.idtable list }
4.87 - | Hasprefs of { prefcategory: string option, prefs: preference list }
4.88 - | Prefval of { name: string, value: string }
4.89 - | Idvalue of { thyname: PgipTypes.objname option,
4.90 - objtype: PgipTypes.objtype,
4.91 - name: PgipTypes.objname,
4.92 - text: XML.tree list }
4.93 - | Setrefs of { url: PgipTypes.pgipurl option,
4.94 - thyname: PgipTypes.objname option,
4.95 - objtype: PgipTypes.objtype option,
4.96 - name: PgipTypes.objname option,
4.97 - idtables: PgipTypes.idtable list,
4.98 - fileurls : PgipTypes.pgipurl list }
4.99 - | Informguise of { file : PgipTypes.pgipurl option,
4.100 - theory: PgipTypes.objname option,
4.101 - theorem: PgipTypes.objname option,
4.102 - proofpos: int option }
4.103 - | Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
4.104 - errs: XML.tree list } (* errs to become PGML *)
4.105 - | Usespgip of { version: string,
4.106 - pgipelems: (string * bool * string list) list }
4.107 - | Usespgml of { version: string }
4.108 - | Pgip of { tag: string option,
4.109 - class: string,
4.110 - seq: int, id: string,
4.111 +datatype pgipoutput =
4.112 + Hasprefs of { prefcategory: string option,
4.113 + prefs: PgipTypes.preference list }
4.114 + | Pgip of { tag: string option,
4.115 + class: string,
4.116 + seq: int, id: string,
4.117 destid: string option,
4.118 refid: string option,
4.119 refseq: int option,
4.120 content: XML.tree list }
4.121 - | Ready of { }
4.122
4.123 -
4.124 -(* Construct output XML messages *)
4.125 -
4.126 -fun normalresponse (Normalresponse vs) =
4.127 +fun output (Hasprefs vs) =
4.128 let
4.129 - val content = #content vs
4.130 - in
4.131 - XML.Elem (("normalresponse", []), content)
4.132 + val prefcategory = #prefcategory vs
4.133 + val prefs = #prefs vs
4.134 + in
4.135 + XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory),
4.136 + map PgipTypes.haspref prefs)
4.137 end
4.138 -
4.139 -fun errorresponse (Errorresponse vs) =
4.140 - let
4.141 - val fatality = #fatality vs
4.142 - val location = #location vs
4.143 - val content = #content vs
4.144 - in
4.145 - XML.Elem (("errorresponse",
4.146 - attrs_of_fatality fatality @
4.147 - these (Option.map attrs_of_location location)),
4.148 - content)
4.149 - end
4.150 -
4.151 -fun informfileloaded (Informfileloaded vs) =
4.152 - let
4.153 - val url = #url vs
4.154 - val completed = #completed vs
4.155 - in
4.156 - XML.Elem (("informfileloaded",
4.157 - attrs_of_pgipurl url @
4.158 - (attr "completed" (PgipTypes.bool_to_pgstring completed))),
4.159 - [])
4.160 - end
4.161 -
4.162 -fun informfileoutdated (Informfileoutdated vs) =
4.163 - let
4.164 - val url = #url vs
4.165 - val completed = #completed vs
4.166 - in
4.167 - XML.Elem (("informfileoutdated",
4.168 - attrs_of_pgipurl url @
4.169 - (attr "completed" (PgipTypes.bool_to_pgstring completed))),
4.170 - [])
4.171 - end
4.172 -
4.173 -fun informfileretracted (Informfileretracted vs) =
4.174 - let
4.175 - val url = #url vs
4.176 - val completed = #completed vs
4.177 - in
4.178 - XML.Elem (("informfileretracted",
4.179 - attrs_of_pgipurl url @
4.180 - (attr "completed" (PgipTypes.bool_to_pgstring completed))),
4.181 - [])
4.182 - end
4.183 -
4.184 -fun metainforesponse (Metainforesponse vs) =
4.185 - let
4.186 - val attrs = #attrs vs
4.187 - val content = #content vs
4.188 - in
4.189 - XML.Elem (("metainforesponse", attrs), content)
4.190 - end
4.191 -
4.192 -fun lexicalstructure (Lexicalstructure vs) =
4.193 + | output (Pgip vs) =
4.194 let
4.195 - val content = #content vs
4.196 - in
4.197 - XML.Elem (("lexicalstructure", []), content)
4.198 - end
4.199 -
4.200 -fun proverinfo (Proverinfo vs) =
4.201 - let
4.202 - val name = #name vs
4.203 - val version = #version vs
4.204 - val instance = #instance vs
4.205 - val descr = #descr vs
4.206 - val url = #url vs
4.207 - val filenameextns = #filenameextns vs
4.208 - in
4.209 - XML.Elem (("proverinfo",
4.210 - [("name", name),
4.211 - ("version", version),
4.212 - ("instance", instance),
4.213 - ("descr", descr),
4.214 - ("url", Url.implode url),
4.215 - ("filenameextns", filenameextns)]),
4.216 - [])
4.217 - end
4.218 -
4.219 -fun setids (Setids vs) =
4.220 - let
4.221 - val idtables = #idtables vs
4.222 - in
4.223 - XML.Elem (("setids", []), map idtable_to_xml idtables)
4.224 - end
4.225 -
4.226 -fun setrefs (Setrefs vs) =
4.227 - let
4.228 - val url = #url vs
4.229 - val thyname = #thyname vs
4.230 - val objtype = #objtype vs
4.231 - val name = #name vs
4.232 - val idtables = #idtables vs
4.233 - val fileurls = #fileurls vs
4.234 - fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
4.235 - in
4.236 - XML.Elem (("setrefs",
4.237 - (the_default [] (Option.map attrs_of_pgipurl url)) @
4.238 - (the_default [] (Option.map attrs_of_objtype objtype)) @
4.239 - (opt_attr "thyname" thyname) @
4.240 - (opt_attr "name" name)),
4.241 - (map idtable_to_xml idtables) @
4.242 - (map fileurl_to_xml fileurls))
4.243 - end
4.244 -
4.245 -fun addids (Addids vs) =
4.246 - let
4.247 - val idtables = #idtables vs
4.248 - in
4.249 - XML.Elem (("addids", []), map idtable_to_xml idtables)
4.250 - end
4.251 -
4.252 -fun delids (Delids vs) =
4.253 - let
4.254 - val idtables = #idtables vs
4.255 - in
4.256 - XML.Elem (("delids", []), map idtable_to_xml idtables)
4.257 - end
4.258 -
4.259 -fun hasprefs (Hasprefs vs) =
4.260 - let
4.261 - val prefcategory = #prefcategory vs
4.262 - val prefs = #prefs vs
4.263 - in
4.264 - XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
4.265 - end
4.266 -
4.267 -fun prefval (Prefval vs) =
4.268 - let
4.269 - val name = #name vs
4.270 - val value = #value vs
4.271 - in
4.272 - XML.Elem (("prefval", attr "name" name), [XML.Text value])
4.273 - end
4.274 -
4.275 -fun idvalue (Idvalue vs) =
4.276 - let
4.277 - val objtype_attrs = attrs_of_objtype (#objtype vs)
4.278 - val thyname = #thyname vs
4.279 - val name = #name vs
4.280 - val text = #text vs
4.281 - in
4.282 - XML.Elem (("idvalue",
4.283 - objtype_attrs @
4.284 - (opt_attr "thyname" thyname) @
4.285 - attr "name" name),
4.286 - text)
4.287 - end
4.288 -
4.289 -fun informguise (Informguise vs) =
4.290 - let
4.291 - val file = #file vs
4.292 - val theory = #theory vs
4.293 - val theorem = #theorem vs
4.294 - val proofpos = #proofpos vs
4.295 -
4.296 - fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
4.297 -
4.298 - val guisefile = elto "guisefile" attrs_of_pgipurl file
4.299 - val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
4.300 - val guiseproof = elto "guiseproof"
4.301 - (fn thm=>(attr "thmname" thm) @
4.302 - (opt_attr "proofpos" (Option.map string_of_int proofpos))) theorem
4.303 - in
4.304 - XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
4.305 - end
4.306 -
4.307 -fun parseresult (Parseresult vs) =
4.308 - let
4.309 - val attrs = #attrs vs
4.310 - val doc = #doc vs
4.311 - val errs = #errs vs
4.312 - val xmldoc = PgipMarkup.output_doc doc
4.313 - in
4.314 - XML.Elem (("parseresult", attrs), errs @ xmldoc)
4.315 - end
4.316 -
4.317 -fun acceptedpgipelems (Usespgip vs) =
4.318 - let
4.319 - val pgipelems = #pgipelems vs
4.320 - fun async_attrs b = if b then attr "async" "true" else []
4.321 - fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
4.322 - fun singlepgipelem (e,async,attrs) =
4.323 - XML.Elem (("pgipelem", async_attrs async @ attrs_attrs attrs), [XML.Text e])
4.324 -
4.325 - in
4.326 - XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
4.327 - end
4.328 -
4.329 -fun usespgip (Usespgip vs) =
4.330 - let
4.331 - val version = #version vs
4.332 - val acceptedelems = acceptedpgipelems (Usespgip vs)
4.333 - in
4.334 - XML.Elem (("usespgip", attr "version" version), [acceptedelems])
4.335 - end
4.336 -
4.337 -fun usespgml (Usespgml vs) =
4.338 - let
4.339 - val version = #version vs
4.340 - in
4.341 - XML.Elem (("usespgml", attr "version" version), [])
4.342 - end
4.343 -
4.344 -fun pgip (Pgip vs) =
4.345 - let
4.346 val tag = #tag vs
4.347 val class = #class vs
4.348 val seq = #seq vs
4.349 @@ -336,41 +54,15 @@
4.350 val content = #content vs
4.351 in
4.352 XML.Elem(("pgip",
4.353 - opt_attr "tag" tag @
4.354 - attr "id" id @
4.355 - opt_attr "destid" destid @
4.356 - attr "class" class @
4.357 - opt_attr "refid" refid @
4.358 - opt_attr_map string_of_int "refseq" refseq @
4.359 - attr "seq" (string_of_int seq)),
4.360 + PgipTypes.opt_attr "tag" tag @
4.361 + PgipTypes.attr "id" id @
4.362 + PgipTypes.opt_attr "destid" destid @
4.363 + PgipTypes.attr "class" class @
4.364 + PgipTypes.opt_attr "refid" refid @
4.365 + PgipTypes.opt_attr_map string_of_int "refseq" refseq @
4.366 + PgipTypes.attr "seq" (string_of_int seq)),
4.367 content)
4.368 end
4.369
4.370 -fun ready (Ready _) = XML.Elem (("ready", []), [])
4.371 -
4.372 -
4.373 -fun output pgipoutput = case pgipoutput of
4.374 - Normalresponse _ => normalresponse pgipoutput
4.375 - | Errorresponse _ => errorresponse pgipoutput
4.376 - | Informfileloaded _ => informfileloaded pgipoutput
4.377 - | Informfileoutdated _ => informfileoutdated pgipoutput
4.378 - | Informfileretracted _ => informfileretracted pgipoutput
4.379 - | Metainforesponse _ => metainforesponse pgipoutput
4.380 - | Lexicalstructure _ => lexicalstructure pgipoutput
4.381 - | Proverinfo _ => proverinfo pgipoutput
4.382 - | Setids _ => setids pgipoutput
4.383 - | Setrefs _ => setrefs pgipoutput
4.384 - | Addids _ => addids pgipoutput
4.385 - | Delids _ => delids pgipoutput
4.386 - | Hasprefs _ => hasprefs pgipoutput
4.387 - | Prefval _ => prefval pgipoutput
4.388 - | Idvalue _ => idvalue pgipoutput
4.389 - | Informguise _ => informguise pgipoutput
4.390 - | Parseresult _ => parseresult pgipoutput
4.391 - | Usespgip _ => usespgip pgipoutput
4.392 - | Usespgml _ => usespgml pgipoutput
4.393 - | Pgip _ => pgip pgipoutput
4.394 - | Ready _ => ready pgipoutput
4.395 -
4.396 end
4.397
5.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML Mon May 13 20:35:04 2013 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,114 +0,0 @@
5.4 -(* Title: Pure/ProofGeneral/pgip_parser.ML
5.5 - Author: David Aspinall and Makarius
5.6 -
5.7 -Parsing theory sources without execution (via keyword classification).
5.8 -*)
5.9 -
5.10 -signature PGIP_PARSER =
5.11 -sig
5.12 - val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
5.13 -end
5.14 -
5.15 -structure PgipParser: PGIP_PARSER =
5.16 -struct
5.17 -
5.18 -structure D = PgipMarkup;
5.19 -structure I = PgipIsabelle;
5.20 -
5.21 -
5.22 -fun badcmd text = [D.Badcmd {text = text}];
5.23 -
5.24 -fun thy_begin text =
5.25 - (case try (Thy_Header.read Position.none) text of
5.26 - NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
5.27 - | SOME {name = (name, _), imports, ...} =>
5.28 - D.Opentheory {thyname = SOME name, parentnames = map #1 imports, text = text})
5.29 - :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
5.30 -
5.31 -fun thy_heading text =
5.32 - [D.Closeblock {},
5.33 - D.Doccomment {text = text},
5.34 - D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
5.35 -
5.36 -fun thy_decl text =
5.37 - [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
5.38 -
5.39 -fun goal text =
5.40 - [D.Opengoal {thmname = NONE, text = text},
5.41 - D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
5.42 -
5.43 -fun prf_block text =
5.44 - [D.Closeblock {},
5.45 - D.Proofstep {text = text},
5.46 - D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
5.47 -
5.48 -fun prf_open text =
5.49 - [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
5.50 - D.Proofstep {text = text}];
5.51 -
5.52 -fun proofstep text = [D.Proofstep {text = text}];
5.53 -fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
5.54 -
5.55 -
5.56 -fun command k f = Symtab.update_new (Keyword.kind_of k, f);
5.57 -
5.58 -val command_keywords = Symtab.empty
5.59 - |> command Keyword.control badcmd
5.60 - |> command Keyword.diag (fn text => [D.Spuriouscmd {text = text}])
5.61 - |> command Keyword.thy_begin thy_begin
5.62 - |> command Keyword.thy_end (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
5.63 - |> command Keyword.thy_heading1 thy_heading
5.64 - |> command Keyword.thy_heading2 thy_heading
5.65 - |> command Keyword.thy_heading3 thy_heading
5.66 - |> command Keyword.thy_heading4 thy_heading
5.67 - |> command Keyword.thy_load thy_decl
5.68 - |> command Keyword.thy_decl thy_decl
5.69 - |> command Keyword.thy_script thy_decl
5.70 - |> command Keyword.thy_goal goal
5.71 - |> command Keyword.qed closegoal
5.72 - |> command Keyword.qed_block closegoal
5.73 - |> command Keyword.qed_global (fn text => [D.Giveupgoal {text = text}])
5.74 - |> command Keyword.prf_heading2 (fn text => [D.Doccomment {text = text}])
5.75 - |> command Keyword.prf_heading3 (fn text => [D.Doccomment {text = text}])
5.76 - |> command Keyword.prf_heading4 (fn text => [D.Doccomment {text = text}])
5.77 - |> command Keyword.prf_goal goal
5.78 - |> command Keyword.prf_block prf_block
5.79 - |> command Keyword.prf_open prf_open
5.80 - |> command Keyword.prf_close (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
5.81 - |> command Keyword.prf_chain proofstep
5.82 - |> command Keyword.prf_decl proofstep
5.83 - |> command Keyword.prf_asm proofstep
5.84 - |> command Keyword.prf_asm_goal goal
5.85 - |> command Keyword.prf_script proofstep;
5.86 -
5.87 -val _ = subset (op =) (map Keyword.kind_of Keyword.kinds, Symtab.keys command_keywords)
5.88 - orelse raise Fail "Incomplete coverage of command keywords";
5.89 -
5.90 -fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
5.91 - | parse_command name text =
5.92 - (case Keyword.command_keyword name of
5.93 - NONE => [D.Unparseable {text = text}]
5.94 - | SOME k =>
5.95 - (case Symtab.lookup command_keywords (Keyword.kind_of k) of
5.96 - NONE => [D.Unparseable {text = text}]
5.97 - | SOME f => f text));
5.98 -
5.99 -fun parse_span span =
5.100 - let
5.101 - val kind = Thy_Syntax.span_kind span;
5.102 - val toks = Thy_Syntax.span_content span;
5.103 - val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
5.104 - in
5.105 - (case kind of
5.106 - Thy_Syntax.Command (name, _) => parse_command name text
5.107 - | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
5.108 - | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
5.109 - end;
5.110 -
5.111 -
5.112 -fun pgip_parser pos str =
5.113 - Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) pos str
5.114 - |> Thy_Syntax.parse_spans
5.115 - |> maps parse_span;
5.116 -
5.117 -end;
6.1 --- a/src/Pure/ProofGeneral/pgml.ML Mon May 13 20:35:04 2013 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,160 +0,0 @@
6.4 -(* Title: Pure/ProofGeneral/pgml.ML
6.5 - Author: David Aspinall
6.6 -
6.7 -PGIP abstraction: PGML
6.8 -*)
6.9 -
6.10 -signature PGML =
6.11 -sig
6.12 - type pgmlsym = { name: string, content: string }
6.13 -
6.14 - datatype pgmlatom = Sym of pgmlsym | Str of string
6.15 -
6.16 - datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
6.17 -
6.18 - datatype pgmlplace = Subscript | Superscript | Above | Below
6.19 -
6.20 - datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
6.21 -
6.22 - datatype pgmlaction = Toggle | Button | Menu
6.23 -
6.24 - datatype pgmlterm =
6.25 - Atoms of { kind: string option, content: pgmlatom list }
6.26 - | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
6.27 - | Break of { mandatory: bool option, indent: int option }
6.28 - | Subterm of { kind: string option,
6.29 - param: string option,
6.30 - place: pgmlplace option,
6.31 - name: string option,
6.32 - decoration: pgmldec option,
6.33 - action: pgmlaction option,
6.34 - pos: string option,
6.35 - xref: PgipTypes.pgipurl option,
6.36 - content: pgmlterm list }
6.37 - | Alt of { kind: string option, content: pgmlterm list }
6.38 - | Embed of XML.tree list
6.39 - | Raw of XML.tree
6.40 -
6.41 - datatype pgml =
6.42 - Pgml of { version: string option, systemid: string option,
6.43 - area: PgipTypes.displayarea option,
6.44 - content: pgmlterm list }
6.45 -
6.46 - val atom_to_xml : pgmlatom -> XML.tree
6.47 - val pgmlterm_to_xml : pgmlterm -> XML.tree
6.48 -
6.49 - val pgml_to_xml : pgml -> XML.tree
6.50 -end
6.51 -
6.52 -
6.53 -structure Pgml : PGML =
6.54 -struct
6.55 - open PgipTypes
6.56 -
6.57 - type pgmlsym = { name: string, content: string }
6.58 -
6.59 - datatype pgmlatom = Sym of pgmlsym | Str of string
6.60 -
6.61 - datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
6.62 -
6.63 - datatype pgmlplace = Subscript | Superscript | Above | Below
6.64 -
6.65 - datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
6.66 -
6.67 - datatype pgmlaction = Toggle | Button | Menu
6.68 -
6.69 - datatype pgmlterm =
6.70 - Atoms of { kind: string option, content: pgmlatom list }
6.71 - | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
6.72 - | Break of { mandatory: bool option, indent: int option }
6.73 - | Subterm of { kind: string option,
6.74 - param: string option,
6.75 - place: pgmlplace option,
6.76 - name: string option,
6.77 - decoration: pgmldec option,
6.78 - action: pgmlaction option,
6.79 - pos: string option,
6.80 - xref: PgipTypes.pgipurl option,
6.81 - content: pgmlterm list }
6.82 - | Alt of { kind: string option, content: pgmlterm list }
6.83 - | Embed of XML.tree list
6.84 - | Raw of XML.tree
6.85 -
6.86 -
6.87 - datatype pgml =
6.88 - Pgml of { version: string option, systemid: string option,
6.89 - area: PgipTypes.displayarea option,
6.90 - content: pgmlterm list }
6.91 -
6.92 - fun pgmlorient_to_string HOVOrient = "hov"
6.93 - | pgmlorient_to_string HOrient = "h"
6.94 - | pgmlorient_to_string VOrient = "v"
6.95 - | pgmlorient_to_string HVOrient = "hv"
6.96 -
6.97 - fun pgmlplace_to_string Subscript = "sub"
6.98 - | pgmlplace_to_string Superscript = "sup"
6.99 - | pgmlplace_to_string Above = "above"
6.100 - | pgmlplace_to_string Below = "below"
6.101 -
6.102 - fun pgmldec_to_string Bold = "bold"
6.103 - | pgmldec_to_string Italic = "italic"
6.104 - | pgmldec_to_string Error = "error"
6.105 - | pgmldec_to_string Warning = "warning"
6.106 - | pgmldec_to_string Info = "info"
6.107 - | pgmldec_to_string (Other s) = "other"
6.108 -
6.109 - fun pgmlaction_to_string Toggle = "toggle"
6.110 - | pgmlaction_to_string Button = "button"
6.111 - | pgmlaction_to_string Menu = "menu"
6.112 -
6.113 - (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
6.114 - would be better not to *) (* FIXME !??? *)
6.115 - fun atom_to_xml (Sym {name, content}) = XML.Elem (("sym", attr "name" name), [XML.Text content])
6.116 - | atom_to_xml (Str content) = XML.Text content;
6.117 -
6.118 - fun pgmlterm_to_xml (Atoms {kind, content}) =
6.119 - XML.Elem(("atom", opt_attr "kind" kind), map atom_to_xml content)
6.120 -
6.121 - | pgmlterm_to_xml (Box {orient, indent, content}) =
6.122 - XML.Elem(("box",
6.123 - opt_attr_map pgmlorient_to_string "orient" orient @
6.124 - opt_attr_map int_to_pgstring "indent" indent),
6.125 - map pgmlterm_to_xml content)
6.126 -
6.127 - | pgmlterm_to_xml (Break {mandatory, indent}) =
6.128 - XML.Elem(("break",
6.129 - opt_attr_map bool_to_pgstring "mandatory" mandatory @
6.130 - opt_attr_map int_to_pgstring "indent" indent), [])
6.131 -
6.132 - | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
6.133 - XML.Elem(("subterm",
6.134 - opt_attr "kind" kind @
6.135 - opt_attr "param" param @
6.136 - opt_attr_map pgmlplace_to_string "place" place @
6.137 - opt_attr "name" name @
6.138 - opt_attr_map pgmldec_to_string "decoration" decoration @
6.139 - opt_attr_map pgmlaction_to_string "action" action @
6.140 - opt_attr "pos" pos @
6.141 - opt_attr_map string_of_pgipurl "xref" xref),
6.142 - map pgmlterm_to_xml content)
6.143 -
6.144 - | pgmlterm_to_xml (Alt {kind, content}) =
6.145 - XML.Elem(("alt", opt_attr "kind" kind), map pgmlterm_to_xml content)
6.146 -
6.147 - | pgmlterm_to_xml (Embed xmls) = XML.Elem(("embed", []), xmls)
6.148 -
6.149 - | pgmlterm_to_xml (Raw xml) = xml
6.150 -
6.151 -
6.152 - datatype pgml =
6.153 - Pgml of { version: string option, systemid: string option,
6.154 - area: PgipTypes.displayarea option,
6.155 - content: pgmlterm list }
6.156 -
6.157 - fun pgml_to_xml (Pgml {version,systemid,area,content}) =
6.158 - XML.Elem(("pgml",
6.159 - opt_attr "version" version @
6.160 - opt_attr "systemid" systemid @
6.161 - the_default [] (Option.map PgipTypes.attrs_of_displayarea area)),
6.162 - map pgmlterm_to_xml content)
6.163 -end
7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 20:35:04 2013 +0200
7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 21:03:30 2013 +0200
7.3 @@ -17,12 +17,6 @@
7.4 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
7.5 struct
7.6
7.7 -open PgipTypes;
7.8 -open PgipMarkup;
7.9 -open PgipInput;
7.10 -open PgipOutput;
7.11 -
7.12 -
7.13 (** print mode **)
7.14
7.15 val proof_general_emacsN = "ProofGeneralEmacs";
7.16 @@ -41,7 +35,7 @@
7.17 fun pgip_serial () = Unsynchronized.inc pgip_seq
7.18
7.19 fun assemble_pgips pgips =
7.20 - Pgip { tag = SOME pgip_tag,
7.21 + PgipOutput.Pgip { tag = SOME pgip_tag,
7.22 class = pgip_class,
7.23 seq = pgip_serial (),
7.24 id = pgip_id,
7.25 @@ -110,7 +104,7 @@
7.26
7.27 local
7.28
7.29 -fun invalid_pgip () = raise PGIP "Invalid PGIP packet received";
7.30 +fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
7.31
7.32 fun output_emacs pgips = Output.urgent_message (output_pgips pgips);
7.33
7.34 @@ -120,7 +114,8 @@
7.35 {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
7.36 in
7.37 ! preferences |> List.app (fn (prefcat, prefs) =>
7.38 - output_emacs [Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
7.39 + output_emacs
7.40 + [PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
7.41 end
7.42 | process_element_emacs (XML.Elem (("setpref", attrs), data)) =
7.43 let
7.44 @@ -157,7 +152,7 @@
7.45 else ()
7.46 end
7.47 | _ => invalid_pgip ())
7.48 - end handle PGIP msg => error (msg ^ "\n" ^ str);
7.49 + end handle PgipTypes.PGIP msg => error (msg ^ "\n" ^ str);
7.50
7.51 val _ =
7.52 Outer_Syntax.improper_command
8.1 --- a/src/Pure/ROOT Mon May 13 20:35:04 2013 +0200
8.2 +++ b/src/Pure/ROOT Mon May 13 21:03:30 2013 +0200
8.3 @@ -160,13 +160,8 @@
8.4 "Proof/proof_rewrite_rules.ML"
8.5 "Proof/proof_syntax.ML"
8.6 "Proof/reconstruct.ML"
8.7 - "ProofGeneral/pgip_input.ML"
8.8 - "ProofGeneral/pgip_isabelle.ML"
8.9 - "ProofGeneral/pgip_markup.ML"
8.10 "ProofGeneral/pgip_output.ML"
8.11 - "ProofGeneral/pgip_parser.ML"
8.12 "ProofGeneral/pgip_types.ML"
8.13 - "ProofGeneral/pgml.ML"
8.14 "ProofGeneral/preferences.ML"
8.15 "ProofGeneral/proof_general_emacs.ML"
8.16 "ProofGeneral/proof_general_pgip.ML"
9.1 --- a/src/Pure/ROOT.ML Mon May 13 20:35:04 2013 +0200
9.2 +++ b/src/Pure/ROOT.ML Mon May 13 21:03:30 2013 +0200
9.3 @@ -299,20 +299,13 @@
9.4 (* configuration for Proof General *)
9.5
9.6 use "ProofGeneral/pgip_types.ML";
9.7 -use "ProofGeneral/pgml.ML";
9.8 -use "ProofGeneral/pgip_markup.ML";
9.9 -use "ProofGeneral/pgip_input.ML";
9.10 use "ProofGeneral/pgip_output.ML";
9.11
9.12 -use "ProofGeneral/pgip_isabelle.ML";
9.13 -
9.14 (use
9.15 |> Unsynchronized.setmp Proofterm.proofs 0
9.16 |> Unsynchronized.setmp Multithreading.max_threads 0)
9.17 "ProofGeneral/preferences.ML";
9.18
9.19 -use "ProofGeneral/pgip_parser.ML";
9.20 -
9.21 use "ProofGeneral/proof_general_pgip.ML";
9.22 use "ProofGeneral/proof_general_emacs.ML";
9.23