let rec get_next_proposition c =
(*
  let msg = Printf.sprintf "get_next_proposition:\nbuffer=%s, pos=%d, searched=%s, prev_prop=(%s, %d)\nalready_proposed=%s"
    c.buffer c.pos c.searched_pattern (fst c.prev_prop) (snd c.prev_prop)
    (String.concat ";" c.already_proposed)
  in
  prerr_endline msg;
*)

  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 (trueList.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