isabelle: src/Pure/System/command_line.ML@a094bf81a496 (annotated)

48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	1	(* Title: Pure/System/command_line.ML
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	2	Author: Makarius
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	3
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	4	Support for Isabelle/ML command line tools.
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	5	*)
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	6
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	7	signature COMMAND_LINE =
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	8	sig
71632 c1bc38327bc2 clarified signature; wenzelm parents: 71631 diff changeset	9	val tool: (unit -> unit) -> unit
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	10	end;
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	11
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	12	structure Command_Line: COMMAND_LINE =
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	13	struct
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	14
78757 a094bf81a496 clarified signature; wenzelm parents: 78725 diff changeset	15	fun tool main =
78720 909dc00766a0 clarified signature; wenzelm parents: 78716 diff changeset	16	Thread_Attributes.uninterruptible_body (fn run =>
56628 a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	17	let
78725 3c02ad5a1586 clarified treatment of exceptions: avoid catch-all handlers; wenzelm parents: 78720 diff changeset	18	fun print_failure exn = (Runtime.exn_error_message exn; Exn.failure_rc exn);
56628 a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	19	val rc =
78757 a094bf81a496 clarified signature; wenzelm parents: 78725 diff changeset	20	(case Exn.capture_body (run main) of
78725 3c02ad5a1586 clarified treatment of exceptions: avoid catch-all handlers; wenzelm parents: 78720 diff changeset	21	Exn.Res () => 0
3c02ad5a1586 clarified treatment of exceptions: avoid catch-all handlers; wenzelm parents: 78720 diff changeset	22	\| Exn.Exn exn =>
3c02ad5a1586 clarified treatment of exceptions: avoid catch-all handlers; wenzelm parents: 78720 diff changeset	23	(case Exn.capture print_failure exn of
3c02ad5a1586 clarified treatment of exceptions: avoid catch-all handlers; wenzelm parents: 78720 diff changeset	24	Exn.Res rc => rc
3c02ad5a1586 clarified treatment of exceptions: avoid catch-all handlers; wenzelm parents: 78720 diff changeset	25	\| Exn.Exn crash => Exn.failure_rc crash));
78720 909dc00766a0 clarified signature; wenzelm parents: 78716 diff changeset	26	in exit rc end);
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	27
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	28	end;

author	wenzelm
	Wed, 11 Oct 2023 11:27:01 +0200
changeset 78757	a094bf81a496
parent 78725	3c02ad5a1586
permissions	-rw-r--r--