ide_utils.ml 1.48 KB
Newer Older
Sylvain Dailler's avatar
Sylvain Dailler committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
(********************)
(* Terminal history *)
(********************)

module History = struct
  type 'a hole_list = 'a list * 'a list

  (* TODO this looks like we can make it more efficient either with imperative
     feature or by being more clever.  With DLlists, we could have added a
     command in O(1). *)
  let add e l =
    match l with
    | ll, lr ->  [], e :: (List.rev ll) @ lr

  let next l =
    match l with
    | ll, [] -> ll, []
    | ll, [hd] -> ll, [hd]
    (* Get acts on the right list so we never empty right list *)
    | ll, cur :: lr -> cur :: ll, lr

  let prev l =
    match l with
    | hd :: ll, lr -> ll, hd :: lr
    | [], lr -> [], lr

  let get l =
    match l with
    | _, hd :: _ -> Some hd
    | _, [] -> None

  type history = {mutable lc : string hole_list;
                   mutable tr : bool}
(* tr is used to know what was the last query from user because cases for the
   first element of the history and other elements is not the same *)

  let create_history () : history =
    {lc = [], [];
     tr = false}

  let get_current h =
    get h.lc

  let print_next_command h =
    if h.tr then
      begin
        h.lc <- next h.lc;
        get_current h
      end
    else
      begin
        let s = get_current h in
        h.tr <- true;
        s
      end

  let print_prev_command h =
    if h.tr then
      begin
        h.lc <- prev h.lc;
        get_current h
      end
    else
      None

  let add_command h e =
    h.lc <- add e h.lc;
    h.tr <- false

end