isabelle: src/Pure/General/output_primitives.ML@ac5e633ad9b3 (annotated)

62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	1	(* Title: Pure/General/output_primitives.ML
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	2	Author: Makarius
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	3
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	4	Primitives for Isabelle output channels.
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	5	*)
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	6
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	7	signature OUTPUT_PRIMITIVES =
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	8	sig
70991 f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	9	structure XML:
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	10	sig
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	11	type attributes = (string * string) list
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	12	datatype tree =
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	13	Elem of (string * attributes) * tree list
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	14	\| Text of string
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	15	type body = tree list
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	16	end
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	17	type output = string
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	18	type serial = int
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	19	type properties = (string * string) list
65301 fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap; wenzelm parents: 62933 diff changeset	20	val ignore_outputs: output list -> unit
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	21	val writeln_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	22	val state_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	23	val information_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	24	val tracing_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	25	val warning_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	26	val legacy_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	27	val error_message_fn: serial * output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	28	val system_message_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	29	val status_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	30	val report_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	31	val result_fn: properties -> output list -> unit
73559 22b5ecb53dd9 more uniform use of Byte_Message; wenzelm parents: 71617 diff changeset	32	type protocol_message_fn = properties -> XML.body list -> unit
70991 f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	33	val protocol_message_fn: protocol_message_fn
62933 f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML; wenzelm parents: 62930 diff changeset	34	val markup_fn: string * properties -> output * output
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	35	end;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	36
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	37	structure Output_Primitives: OUTPUT_PRIMITIVES =
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	38	struct
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	39
70991 f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	40	( XML trees )
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	41
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	42	structure XML =
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	43	struct
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	44
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	45	type attributes = (string * string) list;
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	46
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	47	datatype tree =
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	48	Elem of (string * attributes) * tree list
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	49	\| Text of string;
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	50
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	51	type body = tree list;
71617 01166f13c2c0 tuned whitespace; wenzelm parents: 70991 diff changeset	52
70991 f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	53	end;
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	54
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	55
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	56	(* output *)
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	57
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	58	type output = string;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	59	type serial = int;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	60	type properties = (string * string) list;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	61
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	62	fun ignore_outputs (_: output list) = ();
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	63
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	64	val writeln_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	65	val state_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	66	val information_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	67	val tracing_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	68	val warning_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	69	val legacy_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	70	fun error_message_fn (_: serial, _: output list) = ();
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	71	val system_message_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	72	val status_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	73	val report_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	74	fun result_fn (_: properties) = ignore_outputs;
70991 f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	75
73559 22b5ecb53dd9 more uniform use of Byte_Message; wenzelm parents: 71617 diff changeset	76	type protocol_message_fn = properties -> XML.body list -> unit;
70991 f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required); wenzelm parents: 65301 diff changeset	77	val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	78
62933 f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML; wenzelm parents: 62930 diff changeset	79	fun markup_fn (_: string * properties) = ("", "");
f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML; wenzelm parents: 62930 diff changeset	80
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: diff changeset	81	end;

author	wenzelm
	Tue, 21 Jun 2022 14:51:17 +0200
changeset 75571	ac5e633ad9b3
parent 73559	22b5ecb53dd9
child 80801	090adcdceaae
permissions	-rw-r--r--