37 fun use_file output verbose name = |
37 fun use_file output verbose name = |
38 let |
38 let |
39 val instream = TextIO.openIn name; |
39 val instream = TextIO.openIn name; |
40 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
40 val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
41 in use_text name output verbose txt end; |
41 in use_text name output verbose txt end; |
|
42 |
|
43 |
|
44 |
|
45 (** multithreading **) |
|
46 |
|
47 open Thread; |
|
48 |
|
49 local |
|
50 |
|
51 datatype 'a result = |
|
52 Result of 'a | |
|
53 Exn of exn; |
|
54 |
|
55 fun capture f x = Result (f x) handle e => Exn e; |
|
56 |
|
57 fun release (Result y) = y |
|
58 | release (Exn e) = raise e; |
|
59 |
|
60 fun message s = |
|
61 (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr); |
|
62 |
|
63 |
|
64 val critical_lock = Mutex.mutex (); |
|
65 val critical_thread = ref (NONE: Thread.thread option); |
|
66 |
|
67 in |
|
68 |
|
69 (* critical section -- may be nested within the same thread *) |
|
70 |
|
71 fun self_critical () = |
|
72 (case ! critical_thread of |
|
73 NONE => false |
|
74 | SOME id => Thread.equal (id, Thread.self ())); |
|
75 |
|
76 fun CRITICAL e = |
|
77 if self_critical () then e () |
|
78 else |
|
79 let |
|
80 val _ = |
|
81 if Mutex.trylock critical_lock then () |
|
82 else |
|
83 (message "Waiting for critical lock"; |
|
84 Mutex.lock critical_lock; |
|
85 message "Obtained critical lock"); |
|
86 val _ = critical_thread := SOME (Thread.self ()); |
|
87 val res = capture e (); |
|
88 val _ = critical_thread := NONE; |
|
89 val _ = Mutex.unlock critical_lock; |
|
90 in release res end; |
|
91 |
|
92 end; |