isabelle: src/Pure/ProofGeneral/pgip_output.ML@43fbd02eb9d0 (annotated)

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	Author: David Aspinall
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	3
21940 fbd068dd4d29 minor tuning; wenzelm parents: 21929 diff changeset	4	PGIP abstraction: output commands.
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	5	*)
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	6
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	7	signature PGIPOUTPUT =
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	8	sig
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	9	datatype pgipoutput =
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	10	Hasprefs of { prefcategory: string option,
21649 40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	11	prefs: PgipTypes.preference list }
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	12	\| Pgip of { tag: string option,
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	13	class: string,
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	14	seq: int, id: string,
21649 40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	15	destid: string option,
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	16	refid: string option,
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	17	refseq: int option,
26548 41bbcaf3e481 further cleanup of XML signature; wenzelm parents: 23834 diff changeset	18	content: XML.tree list }
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	19
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	20	val output : pgipoutput -> XML.tree
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	21	end
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	22
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	23	structure PgipOutput : PGIPOUTPUT =
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	24	struct
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	25
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	26	datatype pgipoutput =
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	27	Hasprefs of { prefcategory: string option,
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	28	prefs: PgipTypes.preference list }
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	29	\| Pgip of { tag: string option,
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	30	class: string,
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	31	seq: int, id: string,
21649 40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	32	destid: string option,
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	33	refid: string option,
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	34	refseq: int option,
26548 41bbcaf3e481 further cleanup of XML signature; wenzelm parents: 23834 diff changeset	35	content: XML.tree list }
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	36
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	37	fun output (Hasprefs vs) =
21902 8e5e2571c716 made SML/NJ happy haftmann parents: 21867 diff changeset	38	let
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	39	val prefcategory = #prefcategory vs
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	40	val prefs = #prefs vs
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	41	in
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	42	XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory),
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	43	map PgipTypes.haspref prefs)
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	44	end
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	45	\| output (Pgip vs) =
22161 b2117f4f2d39 Add askrefs, setrefs, error_with_pos aspinall parents: 22040 diff changeset	46	let
21649 40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	47	val tag = #tag vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	48	val class = #class vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	49	val seq = #seq vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	50	val id = #id vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	51	val destid = #destid vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	52	val refid = #refid vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	53	val refseq = #refseq vs
40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	54	val content = #content vs
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	55	in
38228 ada3ab6b9085 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple; wenzelm parents: 33035 diff changeset	56	XML.Elem(("pgip",
51967 43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	57	PgipTypes.opt_attr "tag" tag @
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	58	PgipTypes.attr "id" id @
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	59	PgipTypes.opt_attr "destid" destid @
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	60	PgipTypes.attr "class" class @
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	61	PgipTypes.opt_attr "refid" refid @
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	62	PgipTypes.opt_attr_map string_of_int "refseq" refseq @
43fbd02eb9d0 removed obsolete PGIP material; wenzelm parents: 41491 diff changeset	63	PgipTypes.attr "seq" (string_of_int seq)),
21649 40e6fdd26f82 Support PGIP communication for preferences in Emacs mode. aspinall parents: 21637 diff changeset	64	content)
21637 a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	65	end
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	66
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	67	end
a7b156c404e2 Revamped Proof General interface. aspinall parents: diff changeset	68

author	wenzelm
	Mon, 13 May 2013 21:03:30 +0200
changeset 51967	43fbd02eb9d0
parent 41491	a2ad5b824051
permissions	-rw-r--r--