src/Pure/ProofGeneral/pgip_output.ML
author haftmann
Wed, 27 Dec 2006 16:18:07 +0100
changeset 21902 8e5e2571c716
parent 21867 8750fbc28d5c
child 21929 fb0cd849bc60
permissions -rw-r--r--
made SML/NJ happy
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 }
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    33
    | Setids              of { idtables: PgipTypes.idtable list  }
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    34
    | Delids              of { idtables: PgipTypes.idtable list }
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    35
    | Addids              of { idtables: PgipTypes.idtable list }
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    36
    | Hasprefs            of { prefcategory: string option, 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    37
                               prefs: PgipTypes.preference list }
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    38
    | Prefval             of { name: string, value: string }
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    39
    | Idvalue             of { name: PgipTypes.objname, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    40
			       objtype: PgipTypes.objtype, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    41
			       text: XML.content }
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    42
    | Informguise         of { file : PgipTypes.pgipurl option,  
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    43
                               theory: PgipTypes.objname option, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    44
                               theorem: PgipTypes.objname option, 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    45
                               proofpos: int option }
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    46
    | Parseresult         of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    47
			       errs: XML.content } (* errs to become PGML *)
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 }
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    80
       | Setids              of { idtables: PgipTypes.idtable list  }
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    81
       | Delids              of { idtables: PgipTypes.idtable list }
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    82
       | Addids              of { idtables: PgipTypes.idtable list }
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    83
       | Hasprefs            of { prefcategory: string option, prefs: preference list }
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    84
       | Prefval             of { name: string, value: string }
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    85
       | Idvalue             of { name: PgipTypes.objname, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    86
				  objtype: PgipTypes.objtype, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    87
				  text: XML.content }
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    88
       | Informguise         of { file : PgipTypes.pgipurl option,  
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    89
				  theory: PgipTypes.objname option, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    90
				  theorem: PgipTypes.objname option, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    91
				  proofpos: int option }
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    92
       | Parseresult         of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
    93
				  errs: XML.content } (* errs to become PGML *)
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    94
       | Usespgip            of { version: string, 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    95
                                  pgipelems: (string * bool * string list) list }
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    96
       | Usespgml            of { version: string }
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    97
       | Pgip                of { tag: string option, 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    98
                                  class: string, 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
    99
                                  seq: int, id: string, 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   100
                                  destid: string option,
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   101
                                  refid: string option,
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   102
                                  refseq: int option,
21655
01b2d13153c8 Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents: 21651
diff changeset
   103
                                  content: XML.content }
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   104
       | Ready               of { }
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   105
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   106
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   107
(* Construct output XML messages *)
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   108
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   109
fun cleardisplay (Cleardisplay vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   110
    let
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   111
        val area = #area vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   112
    in
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   113
        XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   114
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   115
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   116
fun normalresponse (Normalresponse vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   117
    let 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   118
        val area = #area vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   119
        val urgent = #urgent vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   120
        val messagecategory = #messagecategory vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   121
        val content = #content vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   122
    in
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   123
        XML.Elem ("normalresponse", 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   124
                 (attrs_of_displayarea area) @
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   125
                 (if urgent then attr "urgent" "true" else []) @
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   126
                 (attrs_of_messagecategory messagecategory),
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   127
                 content)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   128
    end
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   129
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   130
fun errorresponse (Errorresponse vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   131
    let 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   132
        val area = #area vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   133
        val fatality = #fatality vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   134
        val location = #location vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   135
        val content = #content vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   136
    in
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   137
        XML.Elem ("errorresponse",
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   138
                 (the_default [] (Option.map attrs_of_displayarea area)) @
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   139
                 (attrs_of_fatality fatality) @
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   140
                 (the_default [] (Option.map attrs_of_location location)),
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   141
                 content)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   142
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   143
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   144
fun informfileloaded (Informfileloaded vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   145
    let 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   146
        val url = #url vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   147
    in
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   148
        XML.Elem ("informfileloaded", attrs_of_pgipurl url, [])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   149
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   150
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   151
fun informfileretracted (Informfileretracted vs) =
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   152
    let 
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   153
        val url = #url vs
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   154
    in
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   155
        XML.Elem ("informfileretracted", attrs_of_pgipurl url, [])
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   156
    end
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   157
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   158
fun proofstate (Proofstate vs) =
21637
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 pgml = #pgml vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   161
    in
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   162
        XML.Elem("proofstate", [], pgml)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   163
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   164
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   165
fun metainforesponse (Metainforesponse vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   166
    let 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   167
        val attrs = #attrs vs
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 ("metainforesponse", attrs, content)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   171
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   172
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   173
fun lexicalstructure (Lexicalstructure vs) =
21637
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 content = #content vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   176
    in
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   177
        XML.Elem ("lexicalstructure", [], content)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   178
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   179
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   180
fun proverinfo (Proverinfo vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   181
    let
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   182
        val name = #name vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   183
        val version = #version vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   184
        val instance = #instance vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   185
        val descr = #descr vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   186
        val url = #url vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   187
        val filenameextns = #filenameextns vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   188
    in 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   189
        XML.Elem ("proverinfo",
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   190
                 [("name", name),
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   191
                  ("version", version),
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   192
                  ("instance", instance), 
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   193
                  ("descr", descr),
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21655
diff changeset
   194
                  ("url", Url.implode url),
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   195
                  ("filenameextns", filenameextns)],
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   196
                 [])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   197
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   198
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   199
fun setids (Setids vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   200
    let
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   201
        val idtables = #idtables vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   202
    in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   203
        XML.Elem ("setids",[],map idtable_to_xml idtables)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   204
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   205
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   206
fun addids (Addids vs) =
21637
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
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   210
        XML.Elem ("addids",[],map idtable_to_xml idtables)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   211
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   212
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   213
fun delids (Delids vs) =
21637
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
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   217
        XML.Elem ("delids",[],map idtable_to_xml idtables)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   218
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   219
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   220
fun hasprefs (Hasprefs vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   221
  let 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   222
      val prefcategory = #prefcategory vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   223
      val prefs = #prefs vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   224
  in 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   225
      XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   226
  end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   227
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   228
fun prefval (Prefval vs) =
21637
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 name = #name vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   231
        val value = #value vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   232
    in
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   233
        XML.Elem("prefval", attr "name" name, [XML.Text value])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   234
    end 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   235
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   236
fun idvalue (Idvalue vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   237
    let 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   238
        val name = #name vs
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   239
	val objtype_attrs = attrs_of_objtype (#objtype vs)
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   240
        val text = #text vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   241
    in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   242
        XML.Elem("idvalue", attr "name" name @ objtype_attrs, text)
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   243
    end
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   244
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   245
fun informguise (Informguise vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   246
  let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   247
      val file = #file vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   248
      val theory = #theory vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   249
      val theorem = #theorem vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   250
      val proofpos = #proofpos vs
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   251
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   252
      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
   253
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   254
      val guisefile = elto "guisefile" attrs_of_pgipurl file
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   255
      val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   256
      val guiseproof = elto "guiseproof" 
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   257
                            (fn thm=>(attr "thmname" thm) @
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   258
                                     (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   259
  in 
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   260
      XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   261
  end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   262
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   263
fun parseresult (Parseresult vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   264
    let
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   265
        val attrs = #attrs vs
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   266
        val doc = #doc vs
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   267
        val errs = #errs vs
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   268
	val xmldoc = PgipMarkup.output_doc doc
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   269
    in 
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21858
diff changeset
   270
        XML.Elem("parseresult", attrs, errs@xmldoc)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   271
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   272
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   273
fun acceptedpgipelems (Usespgip vs) = 
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   274
    let
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   275
        val pgipelems = #pgipelems vs
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   276
        fun async_attrs b = if b then attr "async" "true" else []
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   277
        fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   278
        fun singlepgipelem (e,async,attrs) = 
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   279
            XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e])
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   280
                                                      
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   281
    in
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   282
        XML.Elem ("acceptedpgipelems", [],
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   283
                 map singlepgipelem pgipelems)
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   284
    end
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   285
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   286
fun usespgip (Usespgip vs) =
21637
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 version = #version vs
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   289
        val acceptedelems = acceptedpgipelems (Usespgip vs)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   290
    in 
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   291
        XML.Elem("usespgip", attr "version" version, [acceptedelems])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   292
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   293
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   294
fun usespgml (Usespgml vs) =
21637
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
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   297
    in 
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   298
        XML.Elem("usespgml", attr "version" version, [])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   299
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   300
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   301
fun pgip (Pgip vs) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   302
    let 
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   303
        val tag = #tag vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   304
        val class = #class vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   305
        val seq = #seq vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   306
        val id = #id vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   307
        val destid = #destid vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   308
        val refid = #refid vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   309
        val refseq = #refseq vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   310
        val content = #content vs
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   311
    in
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   312
        XML.Elem("pgip",
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   313
                 opt_attr "tag" tag @
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   314
                 attr "id" id @
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   315
                 opt_attr "destid" destid @
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   316
                 attr "class" class @
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   317
                 opt_attr "refid" refid @
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   318
                 opt_attr_map string_of_int "refseq" refseq @
21651
99f4a06184dc Fix typo. Some cleanup for XML attributes
aspinall
parents: 21649
diff changeset
   319
                 attr "seq" (string_of_int seq),
21649
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode.
aspinall
parents: 21637
diff changeset
   320
                 content)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   321
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   322
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   323
fun ready (Ready vs) = XML.Elem("ready",[],[])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   324
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   325
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   326
fun output pgipoutput = case pgipoutput of
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   327
 of Cleardisplay _          => cleardisplay pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   328
  | Normalresponse _        => normalresponse pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   329
  | Errorresponse _         => errorresponse pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   330
  | Informfileloaded _      => informfileloaded pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   331
  | Informfileretracted _   => informfileretracted pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   332
  | Proofstate _            => proofstate pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   333
  | Metainforesponse _      => metainforesponse pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   334
  | Lexicalstructure _      => lexicalstructure pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   335
  | Proverinfo _            => proverinfo pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   336
  | Setids _                => setids pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   337
  | Addids _                => addids pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   338
  | Delids _                => delids pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   339
  | Hasprefs _              => hasprefs pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   340
  | Prefval _               => prefval pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   341
  | Idvalue _               => idvalue pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   342
  | Informguise _           => informguise pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   343
  | Parseresult _           => parseresult pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   344
  | Usespgip _              => usespgip pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   345
  | Usespgml _              => usespgml pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   346
  | Pgip _                  => pgip pgipoutput
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   347
  | Ready _                 => ready pgipoutput
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   348
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   349
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   350