src/Pure/ProofGeneral/pgip_output.ML
author aspinall
Mon, 04 Dec 2006 20:40:11 +0100
changeset 21637 a7b156c404e2
child 21649 40e6fdd26f82
permissions -rw-r--r--
Revamped Proof General interface.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/pgip_output.ML
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     2
    ID:         $Id$
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
    Author:     David Aspinall
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     4
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     5
PGIP abstraction: output commands
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     6
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     7
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
signature PGIPOUTPUT =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
sig
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    10
    (* These are the PGIP messages which the prover emits. *) 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    11
    datatype pgipoutput = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    12
	     Cleardisplay        of { area: PgipTypes.displayarea }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    13
	   | Normalresponse      of { area: PgipTypes.displayarea, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    14
				      urgent: bool, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    15
				      messagecategory: PgipTypes.messagecategory, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    16
				      content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    17
	   | Errorresponse       of { fatality: PgipTypes.fatality, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    18
				      area: PgipTypes.displayarea option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    19
				      location: PgipTypes.location option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    20
				      content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    21
	   | Informfileloaded    of { url: PgipTypes.pgipurl }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    22
	   | Informfileretracted of { url: PgipTypes.pgipurl }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    23
	   | Proofstate	         of { pgml: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    24
	   | Metainforesponse    of { attrs: XML.attributes, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    25
				      content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    26
	   | Lexicalstructure    of { content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    27
	   | Proverinfo	         of { name: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    28
				      version: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    29
				      instance: string,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    30
				      descr: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    31
				      url: Url.T, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    32
				      filenameextns: string }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    33
	   | Idtable	         of { objtype: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    34
				      context: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    35
				      ids: string list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    36
           | Setids		 of { idtables: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    37
           | Delids		 of { idtables: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    38
           | Addids		 of { idtables: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    39
	   | Hasprefs	         of { prefcategory: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    40
				      prefs: PgipTypes.preference list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    41
           | Prefval		 of { name: string, value: string }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    42
           | Idvalue		 of { name: string, objtype: string, text: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    43
	   | Informguise	 of { file : PgipTypes.pgipurl option,  
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    44
				      theory: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    45
				      theorem: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    46
				      proofpos: int option }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    47
	   | Parseresult	 of { attrs: XML.attributes, content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    48
           | Usespgip		 of { version: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    49
				      pgipelems: (string * bool * string list) list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    50
           | Usespgml		 of { version: string }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    51
	   | Pgip		 of { tag: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    52
				      class: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    53
				      seq: int, id: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    54
				      destid: string option,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    55
				      refid: string option,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    56
				      refseq: int option,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    57
				      content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    58
	   | Ready		 of { }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    59
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    60
    val output : pgipoutput -> XML.tree					 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    61
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    62
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    63
structure PgipOutput : PGIPOUTPUT =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    64
struct
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    65
open PgipTypes
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    66
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    67
datatype pgipoutput = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    68
	 Cleardisplay        of { area: displayarea }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    69
       | Normalresponse      of { area: displayarea, urgent: bool, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    70
				  messagecategory: messagecategory, content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    71
       | Errorresponse       of { area: displayarea option, fatality: fatality, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    72
				  location: location option, content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    73
       | Informfileloaded    of { url: Path.T }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    74
       | Informfileretracted of { url: Path.T }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    75
       | Proofstate	     of { pgml: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    76
       | Metainforesponse    of { attrs: XML.attributes, content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    77
       | Lexicalstructure    of { content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    78
       | Proverinfo	     of { name: string, version: string, instance: string,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    79
				  descr: string, url: Url.T, filenameextns: string }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    80
       | Idtable	     of { objtype: string, context: string option, ids: string list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    81
       | Setids		     of { idtables: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    82
       | Delids		     of { idtables: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    83
       | Addids		     of { idtables: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    84
       | Hasprefs	     of { prefcategory: string option, prefs: preference list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    85
       | Prefval  	     of { name: string, value: string }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    86
       | Idvalue	     of { name: string, objtype: string, text: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    87
       | Informguise	     of { file : pgipurl option,  theory: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    88
				  theorem: string option, proofpos: int option }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    89
       | Parseresult	     of { attrs: XML.attributes, content: XML.tree list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    90
       | Usespgip	     of { version: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    91
				  pgipelems: (string * bool * string list) list }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    92
       | Usespgml	     of { version: string }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    93
       | Pgip		     of { tag: string option, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    94
				  class: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    95
				  seq: int, id: string, 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    96
				  destid: string option,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    97
				  refid: string option,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    98
				  refseq: int option,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    99
				  content: XML.tree list}
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   100
       | Ready		     of { }
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   101
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   102
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   103
(* util *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   104
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   105
fun attrsome attr f x = case x of NONE => [] | SOME x => [(attr,f x)]
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   106
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   107
(* Construct output XML messages *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   108
	
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   109
fun cleardisplay vs = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   110
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   111
	val area = #area vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   112
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   113
	XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   114
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   115
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   116
fun normalresponse vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   117
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   118
	val area = #area vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   119
	val urgent = #urgent vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   120
	val messagecategory = #messagecategory vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   121
	val content = #content vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   122
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   123
	XML.Elem ("normalresponse", 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   124
		 (attrs_of_displayarea area) @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   125
		 (if urgent then [("urgent", "true")] else []) @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   126
		 (attrs_of_messagecategory messagecategory),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   127
		 content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   128
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   129
				       
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   130
fun errorresponse vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   131
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   132
	val area = #area vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   133
	val fatality = #fatality vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   134
	val location = #location vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   135
	val content = #content vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   136
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   137
	XML.Elem ("errorresponse",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   138
		 (the_default [] (Option.map attrs_of_displayarea area)) @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   139
		 (attrs_of_fatality fatality) @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   140
		 (the_default [] (Option.map attrs_of_location location)),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   141
		 content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   142
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   143
				       
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   144
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   145
fun informfile lr vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   146
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   147
	val url = #url vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   148
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   149
	XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   150
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   151
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   152
val informfileloaded = informfile "loaded"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   153
val informfileretracted = informfile "retracted"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   154
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   155
fun proofstate vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   156
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   157
	val pgml = #pgml vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   158
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   159
	XML.Elem("proofstate", [], pgml)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   160
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   161
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   162
fun metainforesponse vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   163
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   164
	val attrs = #attrs vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   165
	val content = #content vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   166
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   167
	XML.Elem ("metainforesponse", attrs, content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   168
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   169
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   170
fun lexicalstructure vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   171
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   172
	val content = #content vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   173
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   174
	XML.Elem ("lexicalstructure", [], content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   175
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   176
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   177
fun proverinfo vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   178
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   179
	val name = #name vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   180
	val version = #version vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   181
	val instance = #instance vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   182
	val descr = #descr vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   183
	val url = #url vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   184
	val filenameextns = #filenameextns vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   185
    in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   186
	XML.Elem ("proverinfo",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   187
		 [("name", name),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   188
		  ("version", version),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   189
		  ("instance", instance), 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   190
		  ("descr", descr),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   191
		  ("url", Url.pack url),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   192
		  ("filenameextns", filenameextns)],
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   193
		 [])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   194
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   195
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   196
fun idtable vs = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   197
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   198
	val objtype = #objtype vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   199
	val objtype_attrs = [("objtype", objtype)]
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   200
	val context = #context vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   201
	val context_attrs = opt_attr "context" context
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   202
	val ids = #ids vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   203
	val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   204
    in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   205
	XML.Elem ("idtable",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   206
		  objtype_attrs @ context_attrs,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   207
		  ids_content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   208
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   209
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   210
fun setids vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   211
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   212
	val idtables = #idtables vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   213
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   214
	XML.Elem ("setids",[],idtables)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   215
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   216
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   217
fun addids vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   218
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   219
	val idtables = #idtables vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   220
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   221
	XML.Elem ("addids",[],idtables)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   222
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   223
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   224
fun delids vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   225
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   226
	val idtables = #idtables vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   227
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   228
	XML.Elem ("delids",[],idtables)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   229
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   230
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   231
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   232
fun acceptedpgipelems vs = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   233
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   234
	val pgipelems = #pgipelems vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   235
	fun async_attrs b = if b then [("async","true")] else []
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   236
	fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   237
	fun singlepgipelem (e,async,attrs) = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   238
	    XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   239
						      
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   240
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   241
	XML.Elem ("acceptedpgipelems", [],
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   242
		 map singlepgipelem pgipelems)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   243
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   244
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   245
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   246
fun attro x yo = case yo of NONE => [] | SOME y => [(x,y)] : XML.attributes
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   247
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   248
fun hasprefs vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   249
  let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   250
      val prefcategory = #prefcategory vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   251
      val prefs = #prefs vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   252
  in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   253
      XML.Elem("hasprefs",attro "prefcategory" prefcategory, map haspref prefs)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   254
  end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   255
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   256
fun prefval vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   257
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   258
	val name = #name vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   259
	val value = #value vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   260
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   261
	XML.Elem("prefval", [("name",name)], [XML.Text value])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   262
    end 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   263
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   264
fun idvalue vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   265
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   266
	val name = #name vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   267
	val objtype = #objtype vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   268
	val text = #text vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   269
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   270
	XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   271
    end 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   272
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   273
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   274
fun informguise vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   275
  let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   276
      val file = #file vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   277
      val theory = #theory vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   278
      val theorem = #theorem vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   279
      val proofpos = #proofpos vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   280
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   281
      fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])]
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   282
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   283
      val guisefile = elto "guisefile" attrs_of_pgipurl file
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   284
      val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   285
      val guiseproof = elto "guiseproof" 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   286
			    (fn thm=>[("thmname",thm)]@
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   287
				     (attro "proofpos" (Option.map Int.toString proofpos))) theorem
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   288
  in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   289
      XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   290
  end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   291
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   292
fun parseresult vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   293
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   294
	val attrs = #attrs vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   295
	val content = #content vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   296
    in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   297
	XML.Elem("parseresult", attrs, content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   298
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   299
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   300
fun usespgip vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   301
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   302
	val version = #version vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   303
	val acceptedelems = acceptedpgipelems vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   304
    in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   305
	XML.Elem("usespgip", [("version", version)], [acceptedelems])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   306
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   307
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   308
fun usespgml vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   309
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   310
	val version = #version vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   311
    in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   312
	XML.Elem("usespgml", [("version", version)], [])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   313
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   314
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   315
fun pgip vs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   316
    let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   317
	val tag = #tag vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   318
	val class = #class vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   319
	val seq = #seq vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   320
	val id = #id vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   321
	val destid = #destid vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   322
	val refid = #refid vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   323
	val refseq = #refseq vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   324
	val content = #content vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   325
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   326
	XML.Elem("pgip",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   327
		 opt_attr "tag" tag @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   328
		 [("id", id)] @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   329
		 opt_attr "destid" destid @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   330
		 [("class", class)] @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   331
		 opt_attr "refid" refid @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   332
		 opt_attr_map string_of_int "refseq" refseq @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   333
		 [("seq", string_of_int seq)],
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   334
		 content)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   335
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   336
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   337
fun ready vs = 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   338
    XML.Elem("ready",[],[])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   339
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   340
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   341
fun output pgipoutput = case pgipoutput of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   342
   Cleardisplay vs 	   => cleardisplay vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   343
 | Normalresponse vs       => normalresponse vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   344
 | Errorresponse vs        => errorresponse vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   345
 | Informfileloaded vs	   => informfileloaded vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   346
 | Informfileretracted vs  => informfileretracted vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   347
 | Proofstate vs	   => proofstate vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   348
 | Metainforesponse vs	   => metainforesponse vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   349
 | Lexicalstructure vs	   => lexicalstructure vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   350
 | Proverinfo vs	   => proverinfo vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   351
 | Idtable vs		   => idtable vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   352
 | Setids vs		   => setids vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   353
 | Addids vs		   => addids vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   354
 | Delids vs		   => delids vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   355
 | Hasprefs vs		   => hasprefs vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   356
 | Prefval vs		   => prefval vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   357
 | Idvalue vs		   => idvalue vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   358
 | Informguise vs	   => informguise vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   359
 | Parseresult vs	   => parseresult vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   360
 | Usespgip vs		   => usespgip vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   361
 | Usespgml vs		   => usespgml vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   362
 | Pgip vs		   => pgip vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   363
 | Ready vs		   => ready vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   364
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   365
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   366