From c4ffe2b6725a3f8f60763228b77668aa3444f79c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 25 May 2015 14:15:53 +0200
Subject: CoqIDE columns in error and job panels can be sorted.

This grants wish #4194.
---
 ide/session.ml | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/session.ml b/ide/session.ml
index 12b7796633..cfcc592ef1 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
-- 
cgit v1.2.3


From ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 May 2015 15:04:21 +0200
Subject: Jump to error line in CoqIDE grabs focus of the textview.

---
 ide/session.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ide')

diff --git a/ide/session.ml b/ide/session.ml
index cfcc592ef1..fd8f806909 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -296,6 +296,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
         let lno = store#get ~row ~column:(find_int_col "Line" columns) in
         let where = script#buffer#get_iter (`LINE (lno-1)) in
         script#buffer#place_cursor ~where;
+        script#misc#grab_focus ();
         ignore (script#scroll_to_iter
 		  ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
   let tip = GMisc.label ~text:"Double click to jump to error line" () in
-- 
cgit v1.2.3


From 5e873be3cdbdff6b9bad782ce88d2206b9053e14 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 28 May 2015 13:30:06 +0200
Subject: coqide: don't require ocaml >= 4

---
 ide/session.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/session.ml b/ide/session.ml
index fd8f806909..a795f6331a 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -278,8 +278,8 @@ let make_table_widget ?sort cd cb =
     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;
+  CList.iteri make_sorting columns;
+  CList.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)
-- 
cgit v1.2.3