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