src/Pure/ProofGeneral/pgip_output.ML

Support PGIP communication for preferences in Emacs mode.

(*  Title:      Pure/ProofGeneral/pgip_output.ML
    ID:         $Id$
    Author:     David Aspinall

PGIP abstraction: output commands
*)

signature PGIPOUTPUT =
sig
    (* These are the PGIP messages which the prover emits. *) 
    datatype pgipoutput = 
      Cleardisplay        of { area: PgipTypes.displayarea }
    | Normalresponse      of { area: PgipTypes.displayarea, 
                               urgent: bool, 
                               messagecategory: PgipTypes.messagecategory, 
                               content: XML.tree list }
    | Errorresponse       of { fatality: PgipTypes.fatality, 
                               area: PgipTypes.displayarea option, 
                               location: PgipTypes.location option, 
                               content: XML.tree list }
    | Informfileloaded    of { url: PgipTypes.pgipurl }
    | Informfileretracted of { url: PgipTypes.pgipurl }
    | Proofstate          of { pgml: XML.tree list }
    | Metainforesponse    of { attrs: XML.attributes, 
                               content: XML.tree list }
    | Lexicalstructure    of { content: XML.tree list }
    | Proverinfo          of { name: string, 
                               version: string, 
                               instance: string,
                               descr: string, 
                               url: Url.T, 
                               filenameextns: string }
    | Idtable             of { objtype: string, 
                               context: string option, 
                               ids: string list }
    | Setids              of { idtables: XML.tree list }
    | Delids              of { idtables: XML.tree list }
    | Addids              of { idtables: XML.tree list }
    | Hasprefs            of { prefcategory: string option, 
                               prefs: PgipTypes.preference list }
    | Prefval             of { name: string, value: string }
    | Idvalue             of { name: string, objtype: string, text: XML.tree list }
    | Informguise         of { file : PgipTypes.pgipurl option,  
                               theory: string option, 
                               theorem: string option, 
                               proofpos: int option }
    | Parseresult         of { attrs: XML.attributes, content: XML.tree list }
    | Usespgip            of { version: string, 
                               pgipelems: (string * bool * string list) list }
    | Usespgml            of { version: string }
    | Pgip                of { tag: string option, 
                               class: string, 
                               seq: int, id: string, 
                               destid: string option,
                               refid: string option,
                               refseq: int option,
                               content: XML.tree list }
    | Ready               of { }

    val output : pgipoutput -> XML.tree                                  
end

structure PgipOutput : PGIPOUTPUT =
struct
open PgipTypes

datatype pgipoutput = 
         Cleardisplay        of { area: displayarea }
       | Normalresponse      of { area: displayarea, urgent: bool, 
                                  messagecategory: messagecategory, content: XML.tree list }
       | Errorresponse       of { area: displayarea option, fatality: fatality, 
                                  location: location option, content: XML.tree list }
       | Informfileloaded    of { url: Path.T }
       | Informfileretracted of { url: Path.T }
       | Proofstate          of { pgml: XML.tree list }
       | Metainforesponse    of { attrs: XML.attributes, content: XML.tree list }
       | Lexicalstructure    of { content: XML.tree list }
       | Proverinfo          of { name: string, version: string, instance: string,
                                  descr: string, url: Url.T, filenameextns: string }
       | Idtable             of { objtype: string, context: string option, ids: string list }
       | Setids              of { idtables: XML.tree list }
       | Delids              of { idtables: XML.tree list }
       | Addids              of { idtables: XML.tree list }
       | Hasprefs            of { prefcategory: string option, prefs: preference list }
       | Prefval             of { name: string, value: string }
       | Idvalue             of { name: string, objtype: string, text: XML.tree list }
       | Informguise         of { file : pgipurl option,  theory: string option, 
                                  theorem: string option, proofpos: int option }
       | Parseresult         of { attrs: XML.attributes, content: XML.tree list }
       | Usespgip            of { version: string, 
                                  pgipelems: (string * bool * string list) list }
       | Usespgml            of { version: string }
       | Pgip                of { tag: string option, 
                                  class: string, 
                                  seq: int, id: string, 
                                  destid: string option,
                                  refid: string option,
                                  refseq: int option,
                                  content: XML.tree list}
       | Ready               of { }


(* Construct output XML messages *)
        
fun cleardisplay vs = 
    let
        val area = #area vs
    in
        XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
    end

fun normalresponse vs =
    let 
        val area = #area vs
        val urgent = #urgent vs
        val messagecategory = #messagecategory vs
        val content = #content vs
    in
        XML.Elem ("normalresponse", 
                 (attrs_of_displayarea area) @
                 (if urgent then [("urgent", "true")] else []) @
                 (attrs_of_messagecategory messagecategory),
                 content)
    end
                                       
fun errorresponse vs =
    let 
        val area = #area vs
        val fatality = #fatality vs
        val location = #location vs
        val content = #content vs
    in
        XML.Elem ("errorresponse",
                 (the_default [] (Option.map attrs_of_displayarea area)) @
                 (attrs_of_fatality fatality) @
                 (the_default [] (Option.map attrs_of_location location)),
                 content)
    end
                                       

fun informfile lr vs =
    let 
        val url = #url vs
    in
        XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
    end

val informfileloaded = informfile "loaded"
val informfileretracted = informfile "retracted"

fun proofstate vs =
    let
        val pgml = #pgml vs
    in
        XML.Elem("proofstate", [], pgml)
    end

fun metainforesponse vs =
    let 
        val attrs = #attrs vs
        val content = #content vs
    in
        XML.Elem ("metainforesponse", attrs, content)
    end

fun lexicalstructure vs =
    let
        val content = #content vs
    in
        XML.Elem ("lexicalstructure", [], content)
    end

fun proverinfo vs =
    let
        val name = #name vs
        val version = #version vs
        val instance = #instance vs
        val descr = #descr vs
        val url = #url vs
        val filenameextns = #filenameextns vs
    in 
        XML.Elem ("proverinfo",
                 [("name", name),
                  ("version", version),
                  ("instance", instance), 
                  ("descr", descr),
                  ("url", Url.pack url),
                  ("filenameextns", filenameextns)],
                 [])
    end

fun idtable vs = 
    let 
        val objtype = #objtype vs
        val objtype_attrs = attr [("objtype", objtype)]
        val context = #context vs
        val context_attrs = opt_attr "context" context
        val ids = #ids vs
        val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
    in 
        XML.Elem ("idtable",
                  objtype_attrs @ context_attrs,
                  ids_content)
    end

fun setids vs =
    let
        val idtables = #idtables vs
    in
        XML.Elem ("setids",[],idtables)
    end

fun addids vs =
    let
        val idtables = #idtables vs
    in
        XML.Elem ("addids",[],idtables)
    end

fun delids vs =
    let
        val idtables = #idtables vs
    in
        XML.Elem ("delids",[],idtables)
    end


fun acceptedpgipelems vs = 
    let
        val pgipelems = #pgipelems vs
        fun async_attrs b = if b then [("async","true")] else []
        fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
        fun singlepgipelem (e,async,attrs) = 
            XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
                                                      
    in
        XML.Elem ("acceptedpgipelems", [],
                 map singlepgipelem pgipelems)
    end


fun hasprefs vs =
  let 
      val prefcategory = #prefcategory vs
      val prefs = #prefs vs
  in 
      XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
  end

fun prefval vs =
    let 
        val name = #name vs
        val value = #value vs
    in
        XML.Elem("prefval", [("name",name)], [XML.Text value])
    end 

fun idvalue vs =
    let 
        val name = #name vs
        val objtype = #objtype vs
        val text = #text vs
    in
        XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
    end 


fun informguise vs =
  let
      val file = #file vs
      val theory = #theory vs
      val theorem = #theorem vs
      val proofpos = #proofpos vs

      fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])]

      val guisefile = elto "guisefile" attrs_of_pgipurl file
      val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
      val guiseproof = elto "guiseproof" 
                            (fn thm=>[("thmname",thm)]@
                                     (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
  in 
      XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
  end

fun parseresult vs =
    let
        val attrs = #attrs vs
        val content = #content vs
    in 
        XML.Elem("parseresult", attrs, content)
    end

fun usespgip vs =
    let
        val version = #version vs
        val acceptedelems = acceptedpgipelems vs
    in 
        XML.Elem("usespgip", [("version", version)], [acceptedelems])
    end

fun usespgml vs =
    let
        val version = #version vs
    in 
        XML.Elem("usespgml", [("version", version)], [])
    end

fun pgip vs =
    let 
        val tag = #tag vs
        val class = #class vs
        val seq = #seq vs
        val id = #id vs
        val destid = #destid vs
        val refid = #refid vs
        val refseq = #refseq vs
        val content = #content vs
    in
        XML.Elem("pgip",
                 opt_attr "tag" tag @
                 [("id", id)] @
                 opt_attr "destid" destid @
                 [("class", class)] @
                 opt_attr "refid" refid @
                 opt_attr_map string_of_int "refseq" refseq @
                 [("seq", string_of_int seq)],
                 content)
    end

fun ready vs = XML.Elem("ready",[],[])


fun output pgipoutput = case pgipoutput of
   Cleardisplay vs         => cleardisplay vs
 | Normalresponse vs       => normalresponse vs
 | Errorresponse vs        => errorresponse vs
 | Informfileloaded vs     => informfileloaded vs
 | Informfileretracted vs  => informfileretracted vs
 | Proofstate vs           => proofstate vs
 | Metainforesponse vs     => metainforesponse vs
 | Lexicalstructure vs     => lexicalstructure vs
 | Proverinfo vs           => proverinfo vs
 | Idtable vs              => idtable vs
 | Setids vs               => setids vs
 | Addids vs               => addids vs
 | Delids vs               => delids vs
 | Hasprefs vs             => hasprefs vs
 | Prefval vs              => prefval vs
 | Idvalue vs              => idvalue vs
 | Informguise vs          => informguise vs
 | Parseresult vs          => parseresult vs
 | Usespgip vs             => usespgip vs
 | Usespgml vs             => usespgml vs
 | Pgip vs                 => pgip vs
 | Ready vs                => ready vs

end