# HG changeset patch # User wenzelm # Date 1368474147 -7200 # Node ID 1767d4feef7d4c9e3731d0126bc49234f9c8d2fd # Parent b9b2db1e7a5ee7c34f24b9fc4b078c23b38ed31d more direct output of remaining PGIP rudiments; diff -r b9b2db1e7a5e -r 1767d4feef7d src/Pure/ProofGeneral/pgip_output.ML --- a/src/Pure/ProofGeneral/pgip_output.ML Mon May 13 21:07:01 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: Pure/ProofGeneral/pgip_output.ML - Author: David Aspinall - -PGIP abstraction: output commands. -*) - -signature PGIPOUTPUT = -sig - datatype pgipoutput = - Hasprefs of { prefcategory: string option, - prefs: PgipTypes.preference list } - | Pgip of { tag: string option, - class: string, - seq: int, id: string, - destid: string option, - refid: string option, - refseq: int option, - content: XML.tree list } - - val output : pgipoutput -> XML.tree -end - -structure PgipOutput : PGIPOUTPUT = -struct - -datatype pgipoutput = - Hasprefs of { prefcategory: string option, - prefs: PgipTypes.preference list } - | Pgip of { tag: string option, - class: string, - seq: int, id: string, - destid: string option, - refid: string option, - refseq: int option, - content: XML.tree list } - -fun output (Hasprefs vs) = - let - val prefcategory = #prefcategory vs - val prefs = #prefs vs - in - XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory), - map PgipTypes.haspref prefs) - end - | output (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", - PgipTypes.opt_attr "tag" tag @ - PgipTypes.attr "id" id @ - PgipTypes.opt_attr "destid" destid @ - PgipTypes.attr "class" class @ - PgipTypes.opt_attr "refid" refid @ - PgipTypes.opt_attr_map string_of_int "refseq" refseq @ - PgipTypes.attr "seq" (string_of_int seq)), - content) - end - -end - diff -r b9b2db1e7a5e -r 1767d4feef7d src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 21:07:01 2013 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 21:42:27 2013 +0200 @@ -34,21 +34,20 @@ val pgip_seq = Unsynchronized.ref 0 fun pgip_serial () = Unsynchronized.inc pgip_seq - fun assemble_pgips pgips = - PgipOutput.Pgip { tag = SOME pgip_tag, - class = pgip_class, - seq = pgip_serial (), - id = pgip_id, - destid = ! pgip_refid, - (* destid=refid since Isabelle only communicates back to sender *) - refid = ! pgip_refid, - refseq = ! pgip_refseq, - content = pgips } + fun assemble_pgip content = + XML.Elem(("pgip", + [("tag", pgip_tag), ("id", pgip_id)] @ + PgipTypes.opt_attr "destid" (! pgip_refid) @ + [("class", pgip_class)] @ + PgipTypes.opt_attr "refid" (! pgip_refid) @ + PgipTypes.opt_attr_map string_of_int "refseq" (! pgip_refseq) @ + [("seq", string_of_int (pgip_serial ()))]), + content) in fun matching_pgip_id id = (id = pgip_id) -val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; +fun output_pgip content = Output.urgent_message (XML.string_of (assemble_pgip content)); end; @@ -106,16 +105,14 @@ fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received"; -fun output_emacs pgips = Output.urgent_message (output_pgips pgips); - fun process_element_emacs (XML.Elem (("askprefs", _), _)) = let - fun preference_of {name, descr, default, pgiptype, get = _, set = _} = - {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype}; + fun haspref {name, descr, default, pgiptype, get = _, set = _} = + PgipTypes.haspref {name = name, descr = SOME descr, default = SOME default, + pgiptype = pgiptype}; in - ! preferences |> List.app (fn (prefcat, prefs) => - output_emacs - [PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}]) + ! preferences |> List.app (fn (category, prefs) => + output_pgip [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)]) end | process_element_emacs (XML.Elem (("setpref", attrs), data)) = let diff -r b9b2db1e7a5e -r 1767d4feef7d src/Pure/ROOT --- a/src/Pure/ROOT Mon May 13 21:07:01 2013 +0200 +++ b/src/Pure/ROOT Mon May 13 21:42:27 2013 +0200 @@ -160,7 +160,6 @@ "Proof/proof_rewrite_rules.ML" "Proof/proof_syntax.ML" "Proof/reconstruct.ML" - "ProofGeneral/pgip_output.ML" "ProofGeneral/pgip_types.ML" "ProofGeneral/preferences.ML" "ProofGeneral/proof_general_emacs.ML" diff -r b9b2db1e7a5e -r 1767d4feef7d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon May 13 21:07:01 2013 +0200 +++ b/src/Pure/ROOT.ML Mon May 13 21:42:27 2013 +0200 @@ -299,7 +299,6 @@ (* configuration for Proof General *) use "ProofGeneral/pgip_types.ML"; -use "ProofGeneral/pgip_output.ML"; (use |> Unsynchronized.setmp Proofterm.proofs 0