let rec get_next_proposition c =
let buf = fst c.prev_prop in
let res =
try Some (get_next_proposition_in_buffer c buf)
with Not_found ->
None
in
match res with
None ->
begin
match get_next_buffer_in_history buf with
| Some buf ->
c.prev_prop <- (buf, 0);
get_next_proposition c
| None ->
match c.already_proposed with
[] -> None
| l ->
c.already_proposed <- [List.hd (List.rev l)];
c.prev_prop <- (c.buffer, c.pos) ;
Some (true, List.hd (List.rev l))
end
| Some (pos, text) ->
c.prev_prop <- (buf, pos);
if List.mem text c.already_proposed then
get_next_proposition c
else
begin
c.already_proposed <- text :: c.already_proposed;
Some (false, text)
end