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