src/Pure/ProofGeneral/pgip_input.ML
changeset 21637 a7b156c404e2
child 21649 40e6fdd26f82
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Mon Dec 04 20:40:11 2006 +0100
     1.3 @@ -0,0 +1,216 @@
     1.4 +(*  Title:      Pure/ProofGeneral/pgip_input.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     David Aspinall
     1.7 +
     1.8 +PGIP abstraction: input commands
     1.9 +*)
    1.10 +
    1.11 +signature PGIPINPUT =
    1.12 +sig
    1.13 +    (* These are the PGIP commands to which we respond. *) 
    1.14 +    datatype pgipinput = 
    1.15 +       (* protocol/prover config *)
    1.16 +	 Askpgip 	of { }
    1.17 +       | Askpgml 	of { } 
    1.18 +       | Askconfig	of { }
    1.19 +       | Askprefs	of { }
    1.20 +       | Setpref 	of { name:string, prefcategory:string option, value:string }
    1.21 +       | Getpref 	of { name:string, prefcategory:string option }
    1.22 +       (* prover control *)
    1.23 +       | Proverinit 	of { }
    1.24 +       | Proverexit 	of { }
    1.25 +       | Startquiet 	of { }
    1.26 +       | Stopquiet	of { } 
    1.27 +       | Pgmlsymbolson  of { } 
    1.28 +       | Pgmlsymbolsoff of { }
    1.29 +       (* improper proof commands: control proof state *)
    1.30 +       | Dostep		of { text: string }
    1.31 +       | Undostep	of { times: int }
    1.32 +       | Redostep	of { }
    1.33 +       | Abortgoal	of { }
    1.34 +       | Forget		of { thyname: string option, name: string option, 
    1.35 +			     objtype: string option }
    1.36 +       | Restoregoal    of { thmname : string }
    1.37 +       (* context inspection commands *)
    1.38 +       | Askids		of { thyname:string option, objtype:string option }
    1.39 +       | Showid		of { thyname:string option, objtype:string, name:string }
    1.40 +       | Askguise	of { }
    1.41 +       | Parsescript	of { text: string, location: PgipTypes.location,
    1.42 +			     systemdata: string option } 
    1.43 +       | Showproofstate of { }
    1.44 +       | Showctxt	of { }
    1.45 +       | Searchtheorems of { arg: string }
    1.46 +       | Setlinewidth   of { width: int }
    1.47 +       | Viewdoc	of { arg: string }
    1.48 +       (* improper theory-level commands *)
    1.49 +       | Doitem		of { text: string }
    1.50 +       | Undoitem	of { }
    1.51 +       | Redoitem	of { }
    1.52 +       | Aborttheory	of { }
    1.53 +       | Retracttheory  of { thyname: string }
    1.54 +       | Loadfile 	of { url: PgipTypes.pgipurl }
    1.55 +       | Openfile 	of { url: PgipTypes.pgipurl }
    1.56 +       | Closefile	of { }
    1.57 +       | Abortfile	of { }
    1.58 +       | Retractfile    of { url: PgipTypes.pgipurl }
    1.59 +       | Changecwd 	of { url: PgipTypes.pgipurl }
    1.60 +       | Systemcmd 	of { arg: string }
    1.61 +       (* unofficial escape command for debugging *)
    1.62 +       | Quitpgip	of { }
    1.63 +
    1.64 +    val input           : XML.element -> pgipinput option        (* raises PGIP *)
    1.65 +end
    1.66 +
    1.67 +structure PgipInput : PGIPINPUT = 
    1.68 +struct
    1.69 +
    1.70 +open PgipTypes
    1.71 +
    1.72 +(*** PGIP input ***)
    1.73 +
    1.74 +datatype pgipinput = 
    1.75 +	 (* protocol/prover config *)
    1.76 +	 Askpgip 	of { }
    1.77 +       | Askpgml 	of { } 
    1.78 +       | Askconfig	of { }
    1.79 +       | Askprefs	of { }
    1.80 +       | Setpref 	of { name:string, prefcategory:string option, value:string }
    1.81 +       | Getpref 	of { name:string, prefcategory:string option }
    1.82 +       (* prover control *)
    1.83 +       | Proverinit 	of { }
    1.84 +       | Proverexit 	of { }
    1.85 +       | Startquiet 	of { }
    1.86 +       | Stopquiet	of { } 
    1.87 +       | Pgmlsymbolson  of { } 
    1.88 +       | Pgmlsymbolsoff of { }
    1.89 +       (* improper proof commands: control proof state *)
    1.90 +       | Dostep		of { text: string }
    1.91 +       | Undostep	of { times: int }
    1.92 +       | Redostep	of { }
    1.93 +       | Abortgoal	of { }
    1.94 +       | Forget		of { thyname: string option, name: string option, 
    1.95 +			     objtype: string option }
    1.96 +       | Restoregoal    of { thmname : string }
    1.97 +       (* context inspection commands *)
    1.98 +       | Askids		of { thyname:string option, objtype:string option }
    1.99 +       | Showid		of { thyname:string option, objtype:string, name:string }
   1.100 +       | Askguise	of { }
   1.101 +       | Parsescript	of { text: string, location: location,
   1.102 +			     systemdata: string option } 
   1.103 +       | Showproofstate of { }
   1.104 +       | Showctxt	of { }
   1.105 +       | Searchtheorems of { arg: string }
   1.106 +       | Setlinewidth   of { width: int }
   1.107 +       | Viewdoc	of { arg: string }
   1.108 +       (* improper theory-level commands *)
   1.109 +       | Doitem		of { text: string }
   1.110 +       | Undoitem	of { }
   1.111 +       | Redoitem	of { }
   1.112 +       | Aborttheory	of { }
   1.113 +       | Retracttheory  of { thyname: string }
   1.114 +       | Loadfile 	of { url: pgipurl }
   1.115 +       | Openfile 	of { url: pgipurl }
   1.116 +       | Closefile	of { }
   1.117 +       | Abortfile	of { }
   1.118 +       | Retractfile    of { url: pgipurl }
   1.119 +       | Changecwd 	of { url: pgipurl }
   1.120 +       | Systemcmd 	of { arg: string }
   1.121 +       (* unofficial escape command for debugging *)
   1.122 +       | Quitpgip	of { }
   1.123 +
   1.124 +(* Extracting content from input XML elements to make a PGIPinput *)
   1.125 +local
   1.126 +
   1.127 +    val thyname_attro = get_attr_opt "thyname"
   1.128 +    val thyname_attr = get_attr "thyname"
   1.129 +    val objtype_attro = get_attr_opt "objtype"
   1.130 +    val objtype_attr = get_attr "objtype"
   1.131 +    val name_attr = get_attr "name"
   1.132 +    val name_attro = get_attr_opt "name"
   1.133 +    val thmname_attr = get_attr "thmname"
   1.134 +
   1.135 +    val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
   1.136 +    val prefcat_attr = get_attr_opt "prefcategory"
   1.137 +
   1.138 +    fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
   1.139 +      | xmltext [] = ""
   1.140 +      | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
   1.141 +
   1.142 +    exception Unknown
   1.143 +    exception NoAction
   1.144 +in
   1.145 +
   1.146 +(* Return a valid PGIP input command.
   1.147 +   Raise PGIP exception for invalid data.
   1.148 +   Return NONE for unknown/unhandled commands. 
   1.149 +*)
   1.150 +fun input (elem, attrs, data) =
   1.151 +SOME 
   1.152 + (case elem of 
   1.153 +     "askpgip"        => Askpgip { }
   1.154 +   | "askpgml"        => Askpgml { }
   1.155 +   | "askconfig"      => Askconfig { }
   1.156 +   (* proverconfig *)
   1.157 +   | "askprefs"       => Askprefs { }
   1.158 +   | "getpref"        => Getpref { name = name_attr attrs, 
   1.159 +				   prefcategory = prefcat_attr attrs }
   1.160 +   | "setpref"        => Setpref { name = name_attr attrs, 
   1.161 +				   prefcategory = prefcat_attr attrs,
   1.162 +				   value = xmltext data }
   1.163 +   (* provercontrol *)
   1.164 +   | "proverinit"     => Proverinit { }
   1.165 +   | "proverexit"     => Proverexit { }
   1.166 +   | "startquiet"     => Startquiet { }
   1.167 +   | "stopquiet"      => Stopquiet { }
   1.168 +   | "pgmlsymbolson"  => Pgmlsymbolson { }
   1.169 +   (* improperproofcmd: improper commands not in script *)
   1.170 +   | "dostep"         => Dostep    { text = xmltext data }
   1.171 +   | "undostep"       => Undostep  { times = times_attr attrs }
   1.172 +   | "redostep"       => Redostep  { } 
   1.173 +   | "abortgoal"      => Abortgoal { }
   1.174 +   | "forget"         => Forget { thyname = thyname_attro attrs, 
   1.175 +				  name = name_attro attrs,
   1.176 +				  objtype = objtype_attro attrs }
   1.177 +   | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
   1.178 +   (* proofctxt: improper commands *)
   1.179 +   | "askids"         => Askids { thyname = thyname_attro attrs, 
   1.180 +				  objtype = objtype_attro attrs }
   1.181 +   | "showid"         => Showid { thyname = thyname_attro attrs,
   1.182 +				  objtype = objtype_attr attrs,
   1.183 +				  name = name_attr attrs }
   1.184 +   | "askguise"       => Askguise { }
   1.185 +   | "parsescript"    => Parsescript { text = (xmltext data),
   1.186 +				       systemdata = get_attr_opt "systemdata" attrs,
   1.187 +				       location = location_of_attrs attrs }
   1.188 +   | "showproofstate" => Showproofstate { }
   1.189 +   | "showctxt"       => Showctxt { }
   1.190 +   | "searchtheorems" => Searchtheorems { arg = xmltext data }
   1.191 +   | "setlinewidth"   => Setlinewidth   { width = read_pgipnat (xmltext data) }
   1.192 +   | "viewdoc"        => Viewdoc { arg = xmltext data }
   1.193 +   (* improperfilecmd: theory-level commands not in script *)
   1.194 +   | "doitem"         => Doitem  { text = xmltext data }
   1.195 +   | "undoitem"       => Undoitem { }
   1.196 +   | "redoitem"       => Redoitem { }
   1.197 +   | "aborttheory"    => Aborttheory { }
   1.198 +   | "retracttheory"  => Retracttheory { thyname = thyname_attr attrs }
   1.199 +   | "loadfile"       => Loadfile { url = pgipurl_of_attrs attrs }
   1.200 +   | "openfile"       => Openfile { url = pgipurl_of_attrs attrs }
   1.201 +   | "closefile"      => Closefile { }
   1.202 +   | "abortfile"      => Abortfile { }
   1.203 +   | "retractfile"    => Retractfile { url = pgipurl_of_attrs attrs }
   1.204 +   | "changecwd"      => Changecwd { url = pgipurl_of_attrs attrs }
   1.205 +   | "systemcmd"      => Systemcmd { arg = xmltext data }
   1.206 +   (* unofficial command for debugging *)
   1.207 +   | "quitpgip"	=> Quitpgip { }
   1.208 +
   1.209 +   (* We allow sending proper document markup too; we map it back to dostep   *)
   1.210 +   (* and strip out metainfo elements. Markup correctness isn't checked: this *)
   1.211 +   (* is a compatibility measure to make it easy for interfaces.              *)
   1.212 +   | "metainfo"	      => raise NoAction
   1.213 +   | x => if (x mem PgipMarkup.markup_elements)
   1.214 +	     then Dostep { text = xmltext data } (* could use Doitem too *)
   1.215 +	  else raise Unknown) 
   1.216 +    handle Unknown => NONE | NoAction => NONE
   1.217 +end
   1.218 +
   1.219 +end