src/Pure/ProofGeneral/pgip_input.ML
changeset 21649 40e6fdd26f82
parent 21637 a7b156c404e2
child 21655 01b2d13153c8
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Tue Dec 05 01:17:32 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Tue Dec 05 13:56:43 2006 +0100
     1.3 @@ -9,54 +9,54 @@
     1.4  sig
     1.5      (* These are the PGIP commands to which we respond. *) 
     1.6      datatype pgipinput = 
     1.7 -       (* protocol/prover config *)
     1.8 -	 Askpgip 	of { }
     1.9 -       | Askpgml 	of { } 
    1.10 -       | Askconfig	of { }
    1.11 -       | Askprefs	of { }
    1.12 -       | Setpref 	of { name:string, prefcategory:string option, value:string }
    1.13 -       | Getpref 	of { name:string, prefcategory:string option }
    1.14 -       (* prover control *)
    1.15 -       | Proverinit 	of { }
    1.16 -       | Proverexit 	of { }
    1.17 -       | Startquiet 	of { }
    1.18 -       | Stopquiet	of { } 
    1.19 -       | Pgmlsymbolson  of { } 
    1.20 -       | Pgmlsymbolsoff of { }
    1.21 -       (* improper proof commands: control proof state *)
    1.22 -       | Dostep		of { text: string }
    1.23 -       | Undostep	of { times: int }
    1.24 -       | Redostep	of { }
    1.25 -       | Abortgoal	of { }
    1.26 -       | Forget		of { thyname: string option, name: string option, 
    1.27 -			     objtype: string option }
    1.28 -       | Restoregoal    of { thmname : string }
    1.29 -       (* context inspection commands *)
    1.30 -       | Askids		of { thyname:string option, objtype:string option }
    1.31 -       | Showid		of { thyname:string option, objtype:string, name:string }
    1.32 -       | Askguise	of { }
    1.33 -       | Parsescript	of { text: string, location: PgipTypes.location,
    1.34 -			     systemdata: string option } 
    1.35 -       | Showproofstate of { }
    1.36 -       | Showctxt	of { }
    1.37 -       | Searchtheorems of { arg: string }
    1.38 -       | Setlinewidth   of { width: int }
    1.39 -       | Viewdoc	of { arg: string }
    1.40 -       (* improper theory-level commands *)
    1.41 -       | Doitem		of { text: string }
    1.42 -       | Undoitem	of { }
    1.43 -       | Redoitem	of { }
    1.44 -       | Aborttheory	of { }
    1.45 -       | Retracttheory  of { thyname: string }
    1.46 -       | Loadfile 	of { url: PgipTypes.pgipurl }
    1.47 -       | Openfile 	of { url: PgipTypes.pgipurl }
    1.48 -       | Closefile	of { }
    1.49 -       | Abortfile	of { }
    1.50 -       | Retractfile    of { url: PgipTypes.pgipurl }
    1.51 -       | Changecwd 	of { url: PgipTypes.pgipurl }
    1.52 -       | Systemcmd 	of { arg: string }
    1.53 -       (* unofficial escape command for debugging *)
    1.54 -       | Quitpgip	of { }
    1.55 +    (* protocol/prover config *)
    1.56 +      Askpgip        of { }
    1.57 +    | Askpgml        of { } 
    1.58 +    | Askconfig      of { }
    1.59 +    | Askprefs       of { }
    1.60 +    | Setpref        of { name:string, prefcategory:string option, value:string }
    1.61 +    | Getpref        of { name:string, prefcategory:string option }
    1.62 +    (* prover control *)
    1.63 +    | Proverinit     of { }
    1.64 +    | Proverexit     of { }
    1.65 +    | Startquiet     of { }
    1.66 +    | Stopquiet      of { } 
    1.67 +    | Pgmlsymbolson  of { } 
    1.68 +    | Pgmlsymbolsoff of { }
    1.69 +    (* improper proof commands: control proof state *)
    1.70 +    | Dostep         of { text: string }
    1.71 +    | Undostep       of { times: int }
    1.72 +    | Redostep       of { }
    1.73 +    | Abortgoal      of { }
    1.74 +    | Forget         of { thyname: string option, name: string option, 
    1.75 +                          objtype: string option }
    1.76 +    | Restoregoal    of { thmname : string }
    1.77 +    (* context inspection commands *)
    1.78 +    | Askids         of { thyname:string option, objtype:string option }
    1.79 +    | Showid         of { thyname:string option, objtype:string, name:string }
    1.80 +    | Askguise       of { }
    1.81 +    | Parsescript    of { text: string, location: PgipTypes.location,
    1.82 +                          systemdata: string option } 
    1.83 +    | Showproofstate of { }
    1.84 +    | Showctxt       of { }
    1.85 +    | Searchtheorems of { arg: string }
    1.86 +    | Setlinewidth   of { width: int }
    1.87 +    | Viewdoc        of { arg: string }
    1.88 +    (* improper theory-level commands *)
    1.89 +    | Doitem         of { text: string }
    1.90 +    | Undoitem       of { }
    1.91 +    | Redoitem       of { }
    1.92 +    | Aborttheory    of { }
    1.93 +    | Retracttheory  of { thyname: string }
    1.94 +    | Loadfile       of { url: PgipTypes.pgipurl }
    1.95 +    | Openfile       of { url: PgipTypes.pgipurl }
    1.96 +    | Closefile      of { }
    1.97 +    | Abortfile      of { }
    1.98 +    | Retractfile    of { url: PgipTypes.pgipurl }
    1.99 +    | Changecwd      of { url: PgipTypes.pgipurl }
   1.100 +    | Systemcmd      of { arg: string }
   1.101 +    (* unofficial escape command for debugging *)
   1.102 +    | Quitpgip       of { }
   1.103  
   1.104      val input           : XML.element -> pgipinput option        (* raises PGIP *)
   1.105  end