more direct output of remaining PGIP rudiments;
authorwenzelm
Mon May 13 21:42:27 2013 +0200 (2013-05-13)
changeset 519691767d4feef7d
parent 51968 b9b2db1e7a5e
child 51970 f08366cb9fd1
more direct output of remaining PGIP rudiments;
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Mon May 13 21:07:01 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,68 +0,0 @@
     1.4 -(*  Title:      Pure/ProofGeneral/pgip_output.ML
     1.5 -    Author:     David Aspinall
     1.6 -
     1.7 -PGIP abstraction: output commands.
     1.8 -*)
     1.9 -
    1.10 -signature PGIPOUTPUT =
    1.11 -sig
    1.12 -    datatype pgipoutput =
    1.13 -      Hasprefs            of { prefcategory: string option, 
    1.14 -                               prefs: PgipTypes.preference list }
    1.15 -    | Pgip                of { tag: string option,
    1.16 -                               class: string,
    1.17 -                               seq: int, id: string,
    1.18 -                               destid: string option,
    1.19 -                               refid: string option,
    1.20 -                               refseq: int option,
    1.21 -                               content: XML.tree list }
    1.22 -
    1.23 -    val output : pgipoutput -> XML.tree
    1.24 -end
    1.25 -
    1.26 -structure PgipOutput : PGIPOUTPUT =
    1.27 -struct
    1.28 -
    1.29 -datatype pgipoutput =
    1.30 -         Hasprefs            of { prefcategory: string option, 
    1.31 -                                  prefs: PgipTypes.preference list }
    1.32 -  |      Pgip                of { tag: string option,
    1.33 -                                  class: string,
    1.34 -                                  seq: int, id: string,
    1.35 -                                  destid: string option,
    1.36 -                                  refid: string option,
    1.37 -                                  refseq: int option,
    1.38 -                                  content: XML.tree list }
    1.39 -
    1.40 -fun output (Hasprefs vs) =
    1.41 -    let 
    1.42 -        val prefcategory = #prefcategory vs
    1.43 -        val prefs = #prefs vs
    1.44 -    in 
    1.45 -        XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory),
    1.46 -          map PgipTypes.haspref prefs)
    1.47 -    end
    1.48 -  | output (Pgip vs) =
    1.49 -    let
    1.50 -        val tag = #tag vs
    1.51 -        val class = #class vs
    1.52 -        val seq = #seq vs
    1.53 -        val id = #id vs
    1.54 -        val destid = #destid vs
    1.55 -        val refid = #refid vs
    1.56 -        val refseq = #refseq vs
    1.57 -        val content = #content vs
    1.58 -    in
    1.59 -        XML.Elem(("pgip",
    1.60 -                 PgipTypes.opt_attr "tag" tag @
    1.61 -                 PgipTypes.attr "id" id @
    1.62 -                 PgipTypes.opt_attr "destid" destid @
    1.63 -                 PgipTypes.attr "class" class @
    1.64 -                 PgipTypes.opt_attr "refid" refid @
    1.65 -                 PgipTypes.opt_attr_map string_of_int "refseq" refseq @
    1.66 -                 PgipTypes.attr "seq" (string_of_int seq)),
    1.67 -                 content)
    1.68 -    end
    1.69 -
    1.70 -end
    1.71 -
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 21:07:01 2013 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 21:42:27 2013 +0200
     2.3 @@ -34,21 +34,20 @@
     2.4    val pgip_seq = Unsynchronized.ref 0
     2.5    fun pgip_serial () = Unsynchronized.inc pgip_seq
     2.6  
     2.7 -  fun assemble_pgips pgips =
     2.8 -    PgipOutput.Pgip { tag = SOME pgip_tag,
     2.9 -           class = pgip_class,
    2.10 -           seq = pgip_serial (),
    2.11 -           id = pgip_id,
    2.12 -           destid = ! pgip_refid,
    2.13 -           (* destid=refid since Isabelle only communicates back to sender *)
    2.14 -           refid = ! pgip_refid,
    2.15 -           refseq = ! pgip_refseq,
    2.16 -           content = pgips }
    2.17 +  fun assemble_pgip content =
    2.18 +    XML.Elem(("pgip",
    2.19 +             [("tag", pgip_tag), ("id", pgip_id)] @
    2.20 +             PgipTypes.opt_attr "destid" (! pgip_refid) @
    2.21 +             [("class", pgip_class)] @
    2.22 +             PgipTypes.opt_attr "refid" (! pgip_refid) @
    2.23 +             PgipTypes.opt_attr_map string_of_int "refseq" (! pgip_refseq) @
    2.24 +             [("seq", string_of_int (pgip_serial ()))]),
    2.25 +             content)
    2.26  in
    2.27  
    2.28  fun matching_pgip_id id = (id = pgip_id)
    2.29  
    2.30 -val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    2.31 +fun output_pgip content = Output.urgent_message (XML.string_of (assemble_pgip content));
    2.32  
    2.33  end;
    2.34  
    2.35 @@ -106,16 +105,14 @@
    2.36  
    2.37  fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
    2.38  
    2.39 -fun output_emacs pgips = Output.urgent_message (output_pgips pgips);
    2.40 -
    2.41  fun process_element_emacs (XML.Elem (("askprefs", _), _)) =
    2.42        let
    2.43 -        fun preference_of {name, descr, default, pgiptype, get = _, set = _} =
    2.44 -          {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
    2.45 +        fun haspref {name, descr, default, pgiptype, get = _, set = _} =
    2.46 +          PgipTypes.haspref {name = name, descr = SOME descr, default = SOME default,
    2.47 +            pgiptype = pgiptype};
    2.48        in
    2.49 -        ! preferences |> List.app (fn (prefcat, prefs) =>
    2.50 -            output_emacs
    2.51 -              [PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
    2.52 +        ! preferences |> List.app (fn (category, prefs) =>
    2.53 +            output_pgip [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
    2.54        end
    2.55    | process_element_emacs (XML.Elem (("setpref", attrs), data)) =
    2.56        let
     3.1 --- a/src/Pure/ROOT	Mon May 13 21:07:01 2013 +0200
     3.2 +++ b/src/Pure/ROOT	Mon May 13 21:42:27 2013 +0200
     3.3 @@ -160,7 +160,6 @@
     3.4      "Proof/proof_rewrite_rules.ML"
     3.5      "Proof/proof_syntax.ML"
     3.6      "Proof/reconstruct.ML"
     3.7 -    "ProofGeneral/pgip_output.ML"
     3.8      "ProofGeneral/pgip_types.ML"
     3.9      "ProofGeneral/preferences.ML"
    3.10      "ProofGeneral/proof_general_emacs.ML"
     4.1 --- a/src/Pure/ROOT.ML	Mon May 13 21:07:01 2013 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon May 13 21:42:27 2013 +0200
     4.3 @@ -299,7 +299,6 @@
     4.4  (* configuration for Proof General *)
     4.5  
     4.6  use "ProofGeneral/pgip_types.ML";
     4.7 -use "ProofGeneral/pgip_output.ML";
     4.8  
     4.9  (use
    4.10    |> Unsynchronized.setmp Proofterm.proofs 0