isabelle: src/Pure/System/command_line.ML@909dc00766a0 (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
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	15	fun tool body =
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
a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	18	val rc =
78716 97dfba4405e3 tuned signature; wenzelm parents: 78673 diff changeset	19	(run body (); 0) handle exn =>
78673 90b12b919b5f clarified signature (again): follow Isabelle/Java/Scala; wenzelm parents: 78671 diff changeset	20	((Runtime.exn_error_message exn; Exn.failure_rc exn) handle err => Exn.failure_rc err);
78720 909dc00766a0 clarified signature; wenzelm parents: 78716 diff changeset	21	in exit rc end);
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	22
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	23	end;

author	wenzelm
	Tue, 26 Sep 2023 14:42:33 +0200
changeset 78720	909dc00766a0
parent 78716	97dfba4405e3
child 78725	3c02ad5a1586
permissions	-rw-r--r--