--- a/src/Pure/ProofGeneral/pgip_input.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML Wed Aug 27 12:00:28 2008 +0200
@@ -30,15 +30,15 @@
| Restoregoal of { thmname : string }
(* context inspection commands *)
| Askids of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype 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 }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option,
+ name: PgipTypes.objname option }
| Showid of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname }
+ objtype: PgipTypes.objtype,
+ name: PgipTypes.objname }
| Askguise of { }
| Parsescript of { text: string, location: PgipTypes.location,
systemdata: string option }
@@ -74,59 +74,59 @@
(*** 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 }
+ (* 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 { }
+ | 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 }
+ | 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 }
+ 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 }
+ 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 }
+ objtype: PgipTypes.objtype,
+ name: PgipTypes.objname }
+ | Askguise of { }
+ | Parsescript of { text: string, location: location,
+ systemdata: string option }
| Showproofstate of { }
- | Showctxt of { }
+ | Showctxt of { }
| Searchtheorems of { arg: string }
| Setlinewidth of { width: int }
- | Viewdoc of { arg: string }
+ | Viewdoc of { arg: string }
(* improper theory-level commands *)
- | Doitem of { text: string }
- | Undoitem of { }
- | Redoitem of { }
- | Aborttheory of { }
+ | 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 { }
+ | Loadfile of { url: pgipurl }
+ | Openfile of { url: pgipurl }
+ | Closefile of { }
+ | Abortfile of { }
| Retractfile of { url: pgipurl }
- | Changecwd of { url: pgipurl }
- | Systemcmd of { arg: string }
+ | Changecwd of { url: pgipurl }
+ | Systemcmd of { arg: string }
(* unofficial escape command for debugging *)
- | Quitpgip of { }
+ | Quitpgip of { }
(* Extracting content from input XML elements to make a PGIPinput *)
local
@@ -140,12 +140,12 @@
val value_attr = get_attr "value"
fun objtype_attro attrs = if has_attr "objtype" attrs then
- SOME (objtype_of_attrs attrs)
- else NONE
+ SOME (objtype_of_attrs attrs)
+ else NONE
fun pgipurl_attro attrs = if has_attr "url" attrs then
- SOME (pgipurl_of_attrs attrs)
- else NONE
+ 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"
@@ -171,39 +171,39 @@
(* proverconfig *)
| "askprefs" => Askprefs { }
| "getpref" => Getpref { name = name_attr attrs,
- prefcategory = prefcat_attr attrs }
+ prefcategory = prefcat_attr attrs }
| "setpref" => Setpref { name = name_attr attrs,
- prefcategory = prefcat_attr attrs,
- value = xmltext data }
+ prefcategory = prefcat_attr attrs,
+ value = xmltext data }
(* provercontrol *)
| "proverinit" => Proverinit { }
| "proverexit" => Proverexit { }
| "setproverflag" => Setproverflag { flagname = flagname_attr attrs,
- value = read_pgipbool (value_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 }
+ 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 }
+ 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 }
+ 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 }
+ 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 }
+ systemdata = get_attr_opt "systemdata" attrs,
+ location = location_of_attrs attrs }
| "showproofstate" => Showproofstate { }
| "showctxt" => Showctxt { }
| "searchtheorems" => Searchtheorems { arg = xmltext data }
@@ -223,17 +223,17 @@
| "changecwd" => Changecwd { url = pgipurl_of_attrs attrs }
| "systemcmd" => Systemcmd { arg = xmltext data }
(* unofficial command for debugging *)
- | "quitpgip" => Quitpgip { }
+ | "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 (x mem PgipMarkup.doc_markup_elements) then
- if (x mem PgipMarkup.doc_markup_elements_ignored) then
- raise NoAction
- else
- Dostep { text = xmltext data } (* could separate out Doitem too *)
- else raise Unknown)
+ if (x mem PgipMarkup.doc_markup_elements_ignored) then
+ raise NoAction
+ else
+ Dostep { text = xmltext data } (* could separate out Doitem too *)
+ else raise Unknown)
handle Unknown => NONE | NoAction => NONE
end