Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit fa87f063 authored by POTTIER Francois's avatar POTTIER Francois

New function [ErrorReports.expand].

parent 6893bbbe
......@@ -130,4 +130,35 @@ let shorten k text =
"..." ^
String.sub text (n - k) k
(* -------------------------------------------------------------------------- *)
let is_digit c =
let c = Char.code c in
Char.code '0' <= c && c <= Char.code '9'
exception Copy
let expand f text =
let n = String.length text in
let b = Buffer.create n in
let rec loop i =
if i < n then begin
let c, i = text.[i], i + 1 in
loop (
if c <> '$' then raise Copy;
let j = ref i in
while !j < n && is_digit text.[!j] do incr j done;
if i = !j then raise Copy;
let k = int_of_string (String.sub text i (!j - i)) in
Buffer.add_string b (f k);
with Copy ->
(* We reach this point if either [c] is not '$' or [c] is '$'
but is not followed by an integer literal. *)
Buffer.add_char b c;
Buffer.contents b
loop 0
......@@ -70,3 +70,9 @@ val compress: string -> string
text is too long, a fragment in the middle is replaced with an ellipsis. *)
val shorten: int -> string -> string
(* [expand f text] searches [text] for occurrences of [$k], where [k]
is a nonnegative integer literal, and replaces each such occurrence
with the string [f k]. *)
val expand: (int -> string) -> string -> string
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment