Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 273efba6 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Modified IDE historic of commands.

Should now work: bug seems solved.
Also, its functional but less efficient !
parent 47683dda
......@@ -5,6 +5,8 @@ open Gconfig
open Stdlib
open Session_itp
open Controller_itp
open Session_user_interface
open Historic
external reset_gc : unit -> unit = "ml_reset_gc"
......@@ -278,7 +280,7 @@ let init_comp () =
command_entry_completion#set_text_column completion_col;
command_entry#set_completion command_entry_completion;
command_entry#set_completion command_entry_completion
......@@ -287,67 +289,24 @@ let init_comp () =
(* Terminal historic *)
(*********************)
(* TODO use doubly linked list from Batteries.... *)
module Dl = struct
type 'a dl = {content: 'a;
mutable next: 'a dl;
mutable prev: 'a dl}
let prepend dl e =
let rec new_element = {content = e; next = new_element; prev = new_element} in
new_element.next <- dl;
new_element.prev <- dl.prev;
dl.prev.next <- new_element;
dl.prev <- new_element
let create e =
let rec new_element = {content = e; next = new_element; prev = new_element} in
new_element
let prev dl = dl.prev
let next dl = dl.next
let get dl = dl.content
end
open Dl
type historic = {mutable top : string dl; mutable current : string dl}
let list_commands : historic =
let top = create "" in
{ top = top; current = top}
let add_command s =
prepend list_commands.top s;
list_commands.top <- prev list_commands.top;
list_commands.current <- list_commands.top
let next_command () =
list_commands.current <- next list_commands.current
let prev_command () =
list_commands.current <- prev list_commands.current
let get_current () =
get list_commands.current
let list_commands = create_historic()
let _ =
command_entry#event#connect#key_press
~callback:(fun (ev: 'a Gdk.event) ->
match GdkEvent.Key.keyval ev with
| k when k = GdkKeysyms._Up -> (* Arrow up *)
next_command ();
let s = get_current () in
command_entry#set_text s; true
let s = print_next_command list_commands in
(match s with
| None -> true
| Some s ->
(command_entry#set_text s; true))
| k when k = GdkKeysyms._Down -> (* Arrow down *)
prev_command ();
let s = get_current () in
command_entry#set_text s; true
let s = print_prev_command list_commands in
(match s with
| None -> true
| Some s ->
(command_entry#set_text s; true))
| _ -> false
)
......@@ -593,7 +552,7 @@ let interp cmd =
let (_ : GtkSignal.id) =
command_entry#connect#activate
~callback:(fun () -> add_command command_entry#text; interp command_entry#text)
~callback:(fun () -> add_command list_commands command_entry#text; interp command_entry#text)
let get_selected_row_references () =
......
......@@ -53,7 +53,86 @@ let cont_from_files spec usage_str env files provers =
(* return the controller *)
c
(*********************)
(* Terminal historic *)
(*********************)
module type Historic_type = sig
type historic
val create_historic: unit -> historic
val print_next_command: historic -> string option
val print_prev_command: historic -> string option
val add_command: historic -> string -> unit
end
module Historic : Historic_type = 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 historic = {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 historic and other elements is not the same *)
let create_historic () : historic =
{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
(***************** strategies *****************)
......
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