CoqIDE columns in error and job panels can be sorted.

This grants wish #4194.

1 files changed, 16 insertions, 3 deletions

diff --git a/ide/session.ml b/ide/session.ml
index 12b779663..cfcc592ef 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -239,7 +239,7 @@ let find_int_col s l =
 let find_string_col s l =
   match List.assoc s l with `StringC c -> c | _ -> assert false
 
-let make_table_widget cd cb =
+let make_table_widget ?sort cd cb =
   let frame = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC () in
   let columns, store =
     let cols = new GTree.column_list in
@@ -253,6 +253,7 @@ let make_table_widget cd cb =
       ~rules_hint:true ~headers_visible:false
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
+  let () = data#set_headers_clickable true in
   let refresh () =
     let clr = Tags.color_of_string current.background_color in
     data#misc#modify_base [`NORMAL, `COLOR clr]
@@ -268,15 +269,27 @@ let make_table_widget cd cb =
       c#set_sizing `AUTOSIZE;
       c)
     columns cd in
+  let make_sorting i (_, c) =
+    let sort (store : GTree.model) it1 it2 = match c with
+    | `IntC c ->
+      Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
+    | `StringC c ->
+      Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c)
+    in
+    store#set_sort_func i sort
+  in
+  List.iteri make_sorting columns;
+  List.iteri (fun i c -> c#set_sort_column_id i) cols;
   List.iter (fun c -> ignore(data#append_column c)) cols;
   ignore(
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
+  let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in
   frame, (fun f -> f columns store), refresh
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
   let table, access, refresh =
-    make_table_widget
+    make_table_widget ~sort:(0, `ASCENDING)
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
         let row = store#get_iter tp in
@@ -311,7 +324,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
 
 let create_jobpage coqtop coqops : jobpage =
   let table, access, refresh =
-    make_table_widget
+    make_table_widget ~sort:(0, `ASCENDING)
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
         let row = store#get_iter tp in