isabelle: src/Pure/System/command_line.ML@3f02bc5a5a03 (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
71631 3f02bc5a5a03 more accurate treatment of errors; wenzelm parents: 62923 diff changeset	9	exception EXIT of int
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	10	val tool: (unit -> int) -> unit
51312 0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	11	val tool0: (unit -> unit) -> unit
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	12	end;
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	13
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	14	structure Command_Line: COMMAND_LINE =
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	15	struct
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	16
71631 3f02bc5a5a03 more accurate treatment of errors; wenzelm parents: 62923 diff changeset	17	exception EXIT of int;
3f02bc5a5a03 more accurate treatment of errors; wenzelm parents: 62923 diff changeset	18
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	19	fun tool body =
62923 3a122e1e352a clarified bootstrap; wenzelm parents: 62891 diff changeset	20	Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
56628 a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	21	let
a2df9de46060 tuned -- avoid warning about catch-all handler; wenzelm parents: 56303 diff changeset	22	val rc =
71631 3f02bc5a5a03 more accurate treatment of errors; wenzelm parents: 62923 diff changeset	23	restore_attributes body ()
3f02bc5a5a03 more accurate treatment of errors; wenzelm parents: 62923 diff changeset	24	handle EXIT rc => rc
3f02bc5a5a03 more accurate treatment of errors; wenzelm parents: 62923 diff changeset	25	\| exn => 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	26	in exit rc end) ();
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	27
51312 0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	28	fun tool0 body = tool (fn () => (body (); 0));
0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	29
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	30	end;

author	wenzelm
	Mon, 30 Mar 2020 19:39:11 +0200
changeset 71631	3f02bc5a5a03
parent 62923	3a122e1e352a
child 71632	c1bc38327bc2
permissions	-rw-r--r--