1 (* Title: Pure/ML-Systems/mosml.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1999 University of Cambridge
6 Compatibility file for Moscow ML 2.00
8 NOTE: saving images does not work (yet!?), may run it interactively as follows:
11 $ isabelle RAW_ML_SYSTEM
12 > val ml_system = "mosml";
13 > use "ML-Systems/mosml.ML";
17 (** ML system related **)
20 (* Poly/ML emulation *)
34 structure Process = Process
35 structure FileSys = FileSys
38 (*To exit the system with an exit code -- an alternative to ^D *)
39 fun exit 0 = Process.exit Process.success
40 | exit _ = Process.exit Process.failure;
42 (*limit the printing depth*)
44 (Meta.printDepth := n div 2;
45 Meta.printLength := n);
47 (*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
48 (*the documentation refers to an installPP but I couldn't fine it!*)
49 fun make_pp path pprint = ();
50 fun install_pp _ = ();
54 fun ml_prompts p1 p2 = ();
57 (** Compiler-independent timing functions **)
61 (*Note start point for timing*)
63 let val CPUtimer = Timer.startCPUTimer();
64 val time = Timer.checkCPUTimer(CPUtimer)
65 in (CPUtimer,time) end;
67 (*Finish timing and return string*)
68 fun endTiming (CPUtimer, {gc,sys,usr}) =
69 let open Time (*...for Time.toString, Time.+ and Time.- *)
70 val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
71 in "User " ^ toString (usr2-usr) ^
72 " GC " ^ toString (gc2-gc) ^
73 " All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
79 (* ML command execution *)
81 (*Can one redirect 'use' directly to an instream?*)
82 fun use_text _ _ txt =
84 val tmp_name = FileSys.tmpName ();
85 val tmp_file = TextIO.openOut tmp_name;
87 TextIO.output (tmp_file, txt);
88 TextIO.closeOut tmp_file;
90 FileSys.remove tmp_name
95 (** interrupts **) (*Note: may get into race conditions*)
97 (* FIXME proper implementation available? *)
101 fun mask_interrupt f x = f x;
102 fun unmask_interrupt f x = f x;
103 fun exhibit_interrupt f x = f x;
109 (* system command execution *)
111 (*execute Unix command which doesn't take any input from stdin and
112 sends its output to stdout; could be done more easily by Unix.execute,
113 but that function doesn't use the PATH*)
114 fun execute command =
116 val tmp_name = FileSys.tmpName ();
117 val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn
119 val result = TextIO.inputAll is;
122 FileSys.remove tmp_name;
126 (*plain version; with return code*)
128 if Process.system cmd = Process.success then 0 else 1;
133 (*get time of last modification*)
134 fun file_info name = Time.toString (FileSys.modTime name) handle _ => "";
140 (case Process.getEnv var of
145 (* non-ASCII input (see also Thy/use.ML) *)
147 val needs_filtered_use = false;