Merge PR coq#19166: CoqIDE: Make tabs reorderable and fix preference …

…on tabs position

Reviewed-by: jfehrle
Reviewed-by: herbelin
Co-authored-by: jfehrle <[email protected]>

doc/changelog/10-coqide/19166-coqide.rst

@@ -0,0 +1,9 @@
+- **Fixed:**
+  Changing the position of buffer names (top, left,
+  bottom or right) no longer needs a restart
+  (`#19166 <https://github.com/coq/coq/pull/19166>`_,
+  by Sylvain Chiron).
+- **Added:**
+  Document tabs are now reorderable
+  (`#19166 <https://github.com/coq/coq/pull/19166>`_,
+  by Sylvain Chiron).

ide/coqide/configwin_ihm.ml

@@ -679,8 +679,8 @@ let edit ?(with_apply=true)
   let rec iter rep =
     try
       match dialog#run () with
-        | `APPLY  -> config_box#apply; iter Return_apply
-        | `OK -> config_box#apply; destroy (); Return_ok
+        | `APPLY  -> config_box#apply; apply (); iter Return_apply
+        | `OK -> config_box#apply; apply (); destroy (); Return_ok
         | _ -> destroy (); rep
     with
         Failure s ->

ide/coqide/coqide.ml

@@ -155,7 +155,7 @@ let clear_db_highlight ?(retn=false) sn () =
       if List.mem osn notebook#pages then  (* in case destroyed *)
         osn.script#clear_debugging_highlight bp ep;
       if retn then
-        notebook#goto_page (notebook#term_num (fun t1 t2 -> t1 == t2) sn);
+        notebook#goto_term sn;
     | None -> ()
   )
 

ide/coqide/wg_Notebook.ml

@@ -11,56 +11,59 @@
 class ['a] typed_notebook make_page kill_page nb =
 object(self)
   inherit GPack.notebook nb as super
+
   val mutable term_list = []
 
-  method append_term (term:'a) =
-    let tab_label,menu_label,page = make_page term in
-      (* XXX - Temporary hack to compile with archaic lablgtk *)
-    ignore (super#append_page ?tab_label ?menu_label page);
-    let real_pos = super#page_num page in
-    let lower,higher = Util.List.chop real_pos term_list in
-      term_list <- lower@[term]@higher;
-      real_pos
-(* XXX - Temporary hack to compile with archaic lablgtk
-  method insert_term ?(build=default_build) ?pos (term:'a) =
-    let tab_label,menu_label,page = build term in
-    let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
-    let lower,higher = Util.List.chop real_pos term_list in
-      term_list <- lower@[term]@higher;
-      real_pos
- *)
-  method prepend_term (term:'a) =
-    let tab_label,menu_label,page = make_page term in
-      (* XXX - Temporary hack to compile with archaic lablgtk *)
-    ignore (super#prepend_page ?tab_label ?menu_label page);
+  method private get_nth_oid index =
+    (super#get_nth_page index)#misc#get_oid
+
+  method private create_term creator (term: 'a) =
+    let tab_label, menu_label, page = make_page term in
+    (* XXX - Temporary hack to compile with archaic lablgtk *)
+    let _ = creator ?tab_label ?menu_label page in
     let real_pos = super#page_num page in
-    let lower,higher = Util.List.chop real_pos term_list in
-      term_list <- lower@[term]@higher;
-      real_pos
+    term_list <- (page#misc#get_oid, term) :: term_list;
+    super#set_tab_reorderable page true;
+    real_pos
 
-  method set_term (term:'a) =
-    let tab_label,menu_label,page = make_page term in
-    let real_pos = super#current_page in
-      term_list <- Util.List.map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
-      super#set_page ?tab_label ?menu_label page
+  method append_term = self#create_term super#append_page
+  method prepend_term = self#create_term super#prepend_page
+  method insert_term ?pos = self#create_term (super#insert_page ?pos)
 
-  method get_nth_term i =
-    List.nth term_list i
+  method set_term (term: 'a) =
+    let tab_label, menu_label, page = make_page term in
+    let orig_oid = self#get_nth_oid super#current_page in
+    term_list <- List.map
+        (fun (oid, sn) -> if oid = orig_oid then page#misc#get_oid, term else oid, sn) term_list;
+    super#set_page ?tab_label ?menu_label page
 
-  method term_num f p =
-    Util.List.index0 f p term_list
+  method get_nth_term index =
+    List.assoc (self#get_nth_oid index) term_list
 
-  method pages = term_list
+  method pages =
+    let terms_count = List.length term_list in
+    let oid_to_num = Hashtbl.create terms_count in
+    for index = 0 to terms_count - 1 do
+      Hashtbl.add oid_to_num (self#get_nth_oid index) index;
+    done;
+    let term_array = Array.make terms_count None in
+    List.iter (fun (oid, sn) -> term_array.(Hashtbl.find oid_to_num oid) <- Some sn) term_list;
+    Array.fold_right (fun t l -> Option.get t :: l) term_array []
 
   method! remove_page index =
-    term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list;
+    kill_page (self#get_nth_term index);
+    term_list <- List.remove_assoc (self#get_nth_oid index) term_list;
     super#remove_page index
 
   method current_term =
-    List.nth term_list super#current_page
+    if super#current_page < 0 then invalid_arg "current_term";
+    self#get_nth_term super#current_page
 
   method goto_term term =
-    List.iteri (fun i sn -> if sn == term then self#goto_page i) term_list
+    let rec oid_to_num ?(index = 0) oid =
+      if (self#get_nth_oid index) = oid then index else oid_to_num ~index:(index + 1) oid
+    in
+    List.iter (fun (oid, sn) -> if sn == term then super#goto_page (oid_to_num oid)) term_list
 
 end
 

ide/coqide/wg_Notebook.mli

@@ -16,9 +16,9 @@ object
   inherit GPack.notebook
   method append_term : 'a -> int
   method prepend_term : 'a -> int
+  method insert_term : ?pos:int -> 'a -> int
   method set_term : 'a -> unit
   method get_nth_term : int -> 'a
-  method term_num : ('a -> 'a -> bool) -> 'a -> int
   method pages : 'a list
   method remove_page : int -> unit
   method current_term : 'a