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