author | wenzelm |
Mon, 01 Feb 2021 14:01:01 +0100 | |
changeset 73219 | feaf43e23b3a |
parent 62819 | d3ff367a16a0 |
permissions | -rw-r--r-- |
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
1 |
|
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
2 |
fun exit 0 = (OS.Process.exit OS.Process.success): unit |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
3 |
| exit _ = OS.Process.exit OS.Process.failure; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
4 |
|
44154 | 5 |
fun reraise exn = |
6 |
(case PolyML.exceptionLocation exn of |
|
7 |
NONE => raise exn |
|
8 |
| SOME location => PolyML.raiseWithLocation (exn, location)); |
|
9 |
||
44258 | 10 |
fun set_exn_serial i exn = |
11 |
let |
|
12 |
val (file, startLine, endLine) = |
|
13 |
(case PolyML.exceptionLocation exn of |
|
14 |
NONE => ("", 0, 0) |
|
15 |
| SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine)); |
|
16 |
val location = |
|
17 |
{file = file, startLine = startLine, endLine = endLine, |
|
18 |
startPosition = ~ i, endPosition = 0}; |
|
19 |
in PolyML.raiseWithLocation (exn, location) handle e => e end; |
|
20 |
||
21 |
fun get_exn_serial exn = |
|
22 |
(case Option.map #startPosition (PolyML.exceptionLocation exn) of |
|
23 |
NONE => NONE |
|
24 |
| SOME i => if i >= 0 then NONE else SOME (~ i)); |
|
25 |
||
44154 | 26 |
exception Interrupt = SML90.Interrupt; |
27 |
val ord = SML90.ord; |
|
28 |
val chr = SML90.chr; |
|
29 |
val raw_explode = SML90.explode; |
|
30 |
val implode = SML90.implode; |
|
31 |
||
32 |
val pointer_eq = PolyML.pointerEq; |
|
33 |
||
34 |
val exception_trace = PolyML.exception_trace; |
|
35 |
||
36 |
open Thread; |
|
37 |
val seconds = Time.fromReal; |
|
38 |
use "General/exn.ML"; |
|
39 |
use "ML-Systems/multithreading.ML"; |
|
40 |
use "ML-Systems/multithreading_polyml.ML"; |
|
41 |
use "ML-Systems/unsynchronized.ML"; |
|
42 |
||
43 |
use "ML-Systems/ml_pretty.ML"; |
|
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
44 |
|
44154 | 45 |
val pretty_ml = |
46 |
let |
|
47 |
fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) = |
|
48 |
let |
|
49 |
fun property name default = |
|
50 |
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of |
|
51 |
SOME (PolyML.ContextProperty (_, b)) => b |
|
52 |
| NONE => default); |
|
53 |
val bg = property "begin" ""; |
|
54 |
val en = property "end" ""; |
|
55 |
val len' = property "length" len; |
|
56 |
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end |
|
57 |
| convert len (PolyML.PrettyString s) = |
|
58 |
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) |
|
59 |
| convert _ (PolyML.PrettyBreak (wd, _)) = |
|
60 |
ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
|
61 |
in convert "" end; |
|
62 |
||
63 |
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = |
|
64 |
let val context = |
|
65 |
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ |
|
66 |
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) |
|
67 |
in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end |
|
68 |
| ml_pretty (ML_Pretty.String (s, len)) = |
|
69 |
if len = size s then PolyML.PrettyString s |
|
70 |
else PolyML.PrettyBlock |
|
71 |
(0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]) |
|
72 |
| ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) |
|
73 |
| ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0); |
|
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
74 |
|
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
75 |
use "General/basics.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
76 |
use "library.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
77 |
use "General/alist.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
78 |
use "General/table.ML"; |
44149 | 79 |
use "General/graph.ML"; |
44258 | 80 |
use "General/ord_list.ML"; |
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
81 |
|
44151 | 82 |
structure Position = |
83 |
struct |
|
84 |
fun thread_data () = (); |
|
85 |
fun setmp_thread_data () f x = f x; |
|
86 |
end; |
|
87 |
||
88 |
structure Output = |
|
89 |
struct |
|
90 |
type output = string; |
|
91 |
fun escape s : output = s; |
|
92 |
fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); |
|
93 |
fun writeln s = raw_stdout (suffix "\n" s); |
|
94 |
fun warning s = writeln (prefix_lines "### " s); |
|
95 |
fun status (_: string) = (); |
|
96 |
end; |
|
97 |
val writeln = Output.writeln; |
|
98 |
val warning = Output.warning; |
|
99 |
fun print_mode_value () : string list = []; |
|
100 |
||
101 |
use "General/properties.ML"; |
|
102 |
use "General/timing.ML"; |
|
103 |
||
61556 | 104 |
use "Concurrent/standard_thread.ML"; |
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
105 |
use "Concurrent/synchronized.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
106 |
use "General/markup.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
107 |
use "Concurrent/single_assignment.ML"; |
44149 | 108 |
use "Concurrent/time_limit.ML"; |
44258 | 109 |
use "Concurrent/par_exn.ML"; |
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
110 |
use "Concurrent/task_queue.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
111 |
use "Concurrent/future.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
112 |
use "Concurrent/lazy.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
113 |
use "Concurrent/par_list.ML"; |
44151 | 114 |
|
115 |
use "General/queue.ML"; |
|
116 |
use "Concurrent/mailbox.ML"; |
|
44148
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
117 |
use "Concurrent/cache.ML"; |
a34e6e292115
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
wenzelm
parents:
diff
changeset
|
118 |
|
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
61556
diff
changeset
|
119 |
ML_system_pp (fn depth => fn pretty => fn var => |
44150 | 120 |
pretty (Synchronized.value var, depth)); |
121 |
||
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
61556
diff
changeset
|
122 |
ML_system_pp (fn depth => fn pretty => fn x => |
44150 | 123 |
(case Future.peek x of |
124 |
NONE => PolyML.PrettyString "<future>" |
|
125 |
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
126 |
| SOME (Exn.Res y) => pretty (y, depth))); |
|
127 |
||
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
61556
diff
changeset
|
128 |
ML_system_pp (fn depth => fn pretty => fn x => |
44150 | 129 |
(case Lazy.peek x of |
130 |
NONE => PolyML.PrettyString "<lazy>" |
|
131 |
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
132 |
| SOME (Exn.Res y) => pretty (y, depth))); |
|
133 |