src/Pure/ProofGeneral/pgip_input.ML
author wenzelm
Thu Apr 03 21:23:39 2008 +0200 (2008-04-03)
changeset 26548 41bbcaf3e481
parent 23436 343e84195e2c
child 28020 1ff5167592ba
permissions -rw-r--r--
further cleanup of XML signature;
     1 (*  Title:      Pure/ProofGeneral/pgip_input.ML
     2     ID:         $Id$
     3     Author:     David Aspinall
     4 
     5 PGIP abstraction: input commands.
     6 *)
     7 
     8 signature PGIPINPUT =
     9 sig
    10     (* These are the PGIP commands to which we respond. *) 
    11     datatype pgipinput = 
    12     (* protocol/prover config *)
    13       Askpgip        of { }
    14     | Askpgml        of { } 
    15     | Askconfig      of { }
    16     | Askprefs       of { }
    17     | Setpref        of { name:string, prefcategory:string option, value:string }
    18     | Getpref        of { name:string, prefcategory:string option }
    19     (* prover control *)
    20     | Proverinit     of { }
    21     | Proverexit     of { }
    22     | Setproverflag  of { flagname:string, value: bool }
    23     (* improper proof commands: control proof state *)
    24     | Dostep         of { text: string }
    25     | Undostep       of { times: int }
    26     | Redostep       of { }
    27     | Abortgoal      of { }
    28     | Forget         of { thyname: string option, name: string option, 
    29                           objtype: PgipTypes.objtype option }
    30     | Restoregoal    of { thmname : string }
    31     (* context inspection commands *)
    32     | Askids         of { url: PgipTypes.pgipurl option,
    33 			  thyname: PgipTypes.objname option,
    34 			  objtype: PgipTypes.objtype option }
    35     | Askrefs        of { url: PgipTypes.pgipurl option,
    36 			  thyname: PgipTypes.objname option,
    37 			  objtype: PgipTypes.objtype option,
    38 			  name: PgipTypes.objname option }
    39     | Showid         of { thyname: PgipTypes.objname option, 
    40 			  objtype: PgipTypes.objtype, 
    41 			  name: PgipTypes.objname }
    42     | Askguise       of { }
    43     | Parsescript    of { text: string, location: PgipTypes.location,
    44                           systemdata: string option } 
    45     | Showproofstate of { }
    46     | Showctxt       of { }
    47     | Searchtheorems of { arg: string }
    48     | Setlinewidth   of { width: int }
    49     | Viewdoc        of { arg: string }
    50     (* improper theory-level commands *)
    51     | Doitem         of { text: string }
    52     | Undoitem       of { }
    53     | Redoitem       of { }
    54     | Aborttheory    of { }
    55     | Retracttheory  of { thyname: string }
    56     | Loadfile       of { url: PgipTypes.pgipurl }
    57     | Openfile       of { url: PgipTypes.pgipurl }
    58     | Closefile      of { }
    59     | Abortfile      of { }
    60     | Retractfile    of { url: PgipTypes.pgipurl }
    61     | Changecwd      of { url: PgipTypes.pgipurl }
    62     | Systemcmd      of { arg: string }
    63     (* unofficial escape command for debugging *)
    64     | Quitpgip       of { }
    65 
    66     val input: string * XML.attributes * XML.tree list -> pgipinput option  (* raises PGIP *)
    67 end
    68 
    69 structure PgipInput : PGIPINPUT = 
    70 struct
    71 
    72 open PgipTypes
    73 
    74 (*** PGIP input ***)
    75 
    76 datatype pgipinput = 
    77 	 (* protocol/prover config *)
    78 	 Askpgip 	of { }
    79        | Askpgml 	of { } 
    80        | Askconfig	of { }
    81        | Askprefs	of { }
    82        | Setpref 	of { name:string, prefcategory:string option, value:string }
    83        | Getpref 	of { name:string, prefcategory:string option }
    84        (* prover control *)
    85        | Proverinit 	of { }
    86        | Proverexit 	of { }
    87        | Setproverflag  of { flagname:string, value: bool }
    88        (* improper proof commands: control proof state *)
    89        | Dostep		of { text: string }
    90        | Undostep	of { times: int }
    91        | Redostep	of { }
    92        | Abortgoal	of { }
    93        | Forget		of { thyname: string option, name: string option, 
    94 			     objtype: PgipTypes.objtype option }
    95        | Restoregoal    of { thmname : string }
    96        (* context inspection commands *)
    97        | Askids         of { url: PgipTypes.pgipurl option,
    98 			     thyname: PgipTypes.objname option,
    99 			     objtype: PgipTypes.objtype option }
   100        | Askrefs        of { url: PgipTypes.pgipurl option,
   101 			     thyname: PgipTypes.objname option,
   102 			     objtype: PgipTypes.objtype option,
   103 			     name: PgipTypes.objname option }
   104        | Showid         of { thyname: PgipTypes.objname option, 
   105 			     objtype: PgipTypes.objtype, 
   106 			     name: PgipTypes.objname }
   107        | Askguise	of { }
   108        | Parsescript	of { text: string, location: location,
   109 			     systemdata: string option } 
   110        | Showproofstate of { }
   111        | Showctxt	of { }
   112        | Searchtheorems of { arg: string }
   113        | Setlinewidth   of { width: int }
   114        | Viewdoc	of { arg: string }
   115        (* improper theory-level commands *)
   116        | Doitem		of { text: string }
   117        | Undoitem	of { }
   118        | Redoitem	of { }
   119        | Aborttheory	of { }
   120        | Retracttheory  of { thyname: string }
   121        | Loadfile 	of { url: pgipurl }
   122        | Openfile 	of { url: pgipurl }
   123        | Closefile	of { }
   124        | Abortfile	of { }
   125        | Retractfile    of { url: pgipurl }
   126        | Changecwd 	of { url: pgipurl }
   127        | Systemcmd 	of { arg: string }
   128        (* unofficial escape command for debugging *)
   129        | Quitpgip	of { }
   130 
   131 (* Extracting content from input XML elements to make a PGIPinput *)
   132 local
   133 
   134     val thyname_attro = get_attr_opt "thyname"
   135     val thyname_attr = get_attr "thyname"
   136     val name_attr = get_attr "name"
   137     val name_attro = get_attr_opt "name"
   138     val thmname_attr = get_attr "thmname"
   139     val flagname_attr = get_attr "flagname"
   140     val value_attr = get_attr "value"
   141 
   142     fun objtype_attro attrs = if has_attr "objtype" attrs then
   143 				  SOME (objtype_of_attrs attrs)
   144 			      else NONE
   145 
   146     fun pgipurl_attro attrs = if has_attr "url" attrs then
   147 				  SOME (pgipurl_of_attrs attrs)
   148 			      else NONE
   149 
   150     val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
   151     val prefcat_attr = get_attr_opt "prefcategory"
   152 
   153     fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
   154       | xmltext [] = ""
   155       | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
   156 
   157     exception Unknown
   158     exception NoAction
   159 in
   160 
   161 (* Return a valid PGIP input command.
   162    Raise PGIP exception for invalid data.
   163    Return NONE for unknown/unhandled commands. 
   164 *)
   165 fun input (elem, attrs, data) =
   166 SOME 
   167  (case elem of 
   168      "askpgip"        => Askpgip { }
   169    | "askpgml"        => Askpgml { }
   170    | "askconfig"      => Askconfig { }
   171    (* proverconfig *)
   172    | "askprefs"       => Askprefs { }
   173    | "getpref"        => Getpref { name = name_attr attrs, 
   174 				   prefcategory = prefcat_attr attrs }
   175    | "setpref"        => Setpref { name = name_attr attrs, 
   176 				   prefcategory = prefcat_attr attrs,
   177 				   value = xmltext data }
   178    (* provercontrol *)
   179    | "proverinit"     => Proverinit { }
   180    | "proverexit"     => Proverexit { }
   181    | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
   182 					 value = read_pgipbool (value_attr attrs) }
   183    (* improperproofcmd: improper commands not in script *)
   184    | "dostep"         => Dostep    { text = xmltext data }
   185    | "undostep"       => Undostep  { times = times_attr attrs }
   186    | "redostep"       => Redostep  { } 
   187    | "abortgoal"      => Abortgoal { }
   188    | "forget"         => Forget { thyname = thyname_attro attrs, 
   189 				  name = name_attro attrs,
   190 				  objtype = objtype_attro attrs }
   191    | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
   192    (* proofctxt: improper commands *)
   193    | "askids"         => Askids { url = pgipurl_attro attrs,
   194 				  thyname = thyname_attro attrs, 
   195 				  objtype = objtype_attro attrs }
   196    | "askrefs"        => Askrefs { url = pgipurl_attro attrs,
   197 				   thyname = thyname_attro attrs, 
   198 				   objtype = objtype_attro attrs,
   199 				   name = name_attro attrs }
   200    | "showid"         => Showid { thyname = thyname_attro attrs,
   201 				  objtype = objtype_of_attrs attrs,
   202 				  name = name_attr attrs }
   203    | "askguise"       => Askguise { }
   204    | "parsescript"    => Parsescript { text = (xmltext data),
   205 				       systemdata = get_attr_opt "systemdata" attrs,
   206 				       location = location_of_attrs attrs }
   207    | "showproofstate" => Showproofstate { }
   208    | "showctxt"       => Showctxt { }
   209    | "searchtheorems" => Searchtheorems { arg = xmltext data }
   210    | "setlinewidth"   => Setlinewidth   { width = read_pgipnat (xmltext data) }
   211    | "viewdoc"        => Viewdoc { arg = xmltext data }
   212    (* improperfilecmd: theory-level commands not in script *)
   213    | "doitem"         => Doitem  { text = xmltext data }
   214    | "undoitem"       => Undoitem { }
   215    | "redoitem"       => Redoitem { }
   216    | "aborttheory"    => Aborttheory { }
   217    | "retracttheory"  => Retracttheory { thyname = thyname_attr attrs }
   218    | "loadfile"       => Loadfile { url = pgipurl_of_attrs attrs }
   219    | "openfile"       => Openfile { url = pgipurl_of_attrs attrs }
   220    | "closefile"      => Closefile { }
   221    | "abortfile"      => Abortfile { }
   222    | "retractfile"    => Retractfile { url = pgipurl_of_attrs attrs }
   223    | "changecwd"      => Changecwd { url = pgipurl_of_attrs attrs }
   224    | "systemcmd"      => Systemcmd { arg = xmltext data }
   225    (* unofficial command for debugging *)
   226    | "quitpgip"	=> Quitpgip { }
   227 
   228    (* We allow sending proper document markup too; we map it back to dostep   *)
   229    (* and strip out metainfo elements. Markup correctness isn't checked: this *)
   230    (* is a compatibility measure to make it easy for interfaces.              *)
   231    | x => if (x mem PgipMarkup.doc_markup_elements) then
   232 	      if (x mem PgipMarkup.doc_markup_elements_ignored) then
   233 		  raise NoAction
   234 	      else 
   235 		  Dostep { text = xmltext data } (* could separate out Doitem too *)
   236 	  else raise Unknown) 
   237     handle Unknown => NONE | NoAction => NONE
   238 end
   239 
   240 end