isabelle: src/Pure/System/command_line.ML@b05aca9cee75 (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
48731 a45ba78abcc1 more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point; wenzelm parents: 48681 diff changeset	9	val tool: (unit -> int) -> unit
51312 0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	10	val tool0: (unit -> unit) -> unit
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	11	end;
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	12
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	13	structure Command_Line: COMMAND_LINE =
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	14	struct
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	15
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	16	fun tool body =
62923 3a122e1e352a clarified bootstrap; wenzelm parents: 62891 diff changeset	17	Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
56628 a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	18	let
a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	19	val rc =
a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	20	restore_attributes body () handle exn =>
56630 d06c44532706 clarified exit code for the rare situation where Runtime.exn_error_message might fail; wenzelm parents: 56628 diff changeset	21	Exn.capture_exit 2 (fn () => (Runtime.exn_error_message exn; raise exn)) ();
62470 9037ed690e19 proper exit as in Scala version (in contrast to a45ba78abcc1); wenzelm parents: 56630 diff changeset	22	in exit rc end) ();
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	23
51312 0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	24	fun tool0 body = tool (fn () => (body (); 0));
0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	25
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	26	end;
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	27

author	wenzelm
	Sun, 12 Jan 2020 22:54:42 +0100
changeset 71370	b05aca9cee75
parent 62923	3a122e1e352a
child 71631	3f02bc5a5a03
permissions	-rw-r--r--