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