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