equal
deleted
inserted
replaced
89 Interrupted | |
89 Interrupted | |
90 Crashed | |
90 Crashed | |
91 InternalError | |
91 InternalError | |
92 UnknownError of string |
92 UnknownError of string |
93 |
93 |
94 fun elide_string threshold s = |
|
95 if size s > threshold then |
|
96 String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ |
|
97 String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) |
|
98 else |
|
99 s |
|
100 fun short_output verbose output = |
94 fun short_output verbose output = |
101 if verbose then |
95 if verbose then |
102 if output = "" then "No details available" else elide_string 1000 output |
96 if output = "" then "No details available" else elide_string 1000 output |
103 else |
97 else |
104 "" |
98 "" |