isabelle: src/Pure/System/command_line.ML@2944cc4f4f56 (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 =
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	17	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)) ();
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	22	in if rc = 0 then () else 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
	Fri, 17 Apr 2015 22:15:35 +0200
changeset 60125	2944cc4f4f56
parent 56630	d06c44532706
child 62470	9037ed690e19
permissions	-rw-r--r--