isabelle: src/Pure/System/command_line.ML@52c22561996d (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 () =>
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	18	let val rc =
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	19	restore_attributes body () handle exn =>
52686 f4871fe80410 more robust exn_messages_ids; wenzelm parents: 51312 diff changeset	20	let
f4871fe80410 more robust exn_messages_ids; wenzelm parents: 51312 diff changeset	21	val _ =
54387 890e983cb07b tuned signature; wenzelm parents: 52686 diff changeset	22	ML_Compiler.exn_error_message exn
890e983cb07b tuned signature; wenzelm parents: 52686 diff changeset	23	handle _ => Output.error_message "Exception raised, but failed to print details!";
52686 f4871fe80410 more robust exn_messages_ids; wenzelm parents: 51312 diff changeset	24	in if Exn.is_interrupt exn then 130 else 1 end;
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	25	in if rc = 0 then () else exit rc end) ();
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	26
51312 0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	27	fun tool0 body = tool (fn () => (body (); 0));
0ce544fbb509 more robust build error handling, e.g. missing outer syntax commands; wenzelm parents: 48731 diff changeset	28
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	29	end;
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: diff changeset	30

author	wenzelm
	Fri, 07 Mar 2014 20:46:27 +0100
changeset 55987	52c22561996d
parent 54387	890e983cb07b
child 56303	4cc3f4db3447
permissions	-rw-r--r--