equal
deleted
inserted
replaced
14 |
14 |
15 fun reraise exn = |
15 fun reraise exn = |
16 (case PolyML.exceptionLocation exn of |
16 (case PolyML.exceptionLocation exn of |
17 NONE => raise exn |
17 NONE => raise exn |
18 | SOME location => PolyML.raiseWithLocation (exn, location)); |
18 | SOME location => PolyML.raiseWithLocation (exn, location)); |
|
19 |
|
20 fun set_exn_serial i exn = |
|
21 let |
|
22 val (file, startLine, endLine) = |
|
23 (case PolyML.exceptionLocation exn of |
|
24 NONE => ("", 0, 0) |
|
25 | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine)); |
|
26 val location = |
|
27 {file = file, startLine = startLine, endLine = endLine, |
|
28 startPosition = ~ i, endPosition = 0}; |
|
29 in PolyML.raiseWithLocation (exn, location) handle e => e end; |
|
30 |
|
31 fun get_exn_serial exn = |
|
32 (case Option.map #startPosition (PolyML.exceptionLocation exn) of |
|
33 NONE => NONE |
|
34 | SOME i => if i >= 0 then NONE else SOME (~ i)); |
19 |
35 |
20 use "ML-Systems/polyml_common.ML"; |
36 use "ML-Systems/polyml_common.ML"; |
21 use "ML-Systems/multithreading_polyml.ML"; |
37 use "ML-Systems/multithreading_polyml.ML"; |
22 use "ML-Systems/unsynchronized.ML"; |
38 use "ML-Systems/unsynchronized.ML"; |
23 |
39 |