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