source displayed + source location in labels

src/core/ident.ml

@@ -67,8 +67,42 @@ let create_ident name origin labels = {
   id_tag    = Hashweak.dummy_tag;
 }
 
+let file_regexp = Str.regexp "file:\\(.*\\)"
+let line_regexp = Str.regexp "line:\\([0-9]+\\)"
+let begin_regexp = Str.regexp "begin:\\([0-9]+\\)"
+let end_regexp = Str.regexp "end:\\([0-9]+\\)"
+
 let id_fresh ?(labels = []) nm = create_ident nm Fresh labels
-let id_user ?(labels = []) nm loc = create_ident nm (User loc) labels
+let id_user ?(labels = []) nm loc =
+  let (f,li,b,e) = Loc.extract loc in
+  let f = ref f in
+  let li = ref li in
+  let b = ref b in
+  let e = ref e in
+  let l = List.fold_left
+    (fun acc ((s,_) as lab) ->
+       if Str.string_match file_regexp s 0 then
+         (f := Str.matched_group 1 s; acc)
+       else
+       if Str.string_match line_regexp s 0 then
+         (li := int_of_string (Str.matched_group 1 s); acc)
+       else
+       if Str.string_match begin_regexp s 0 then
+         (b := int_of_string (Str.matched_group 1 s); acc)
+       else
+       if Str.string_match end_regexp s 0 then
+         (e := int_of_string (Str.matched_group 1 s); acc)
+       else lab :: acc)
+    [] labels
+  in
+  let loc =
+    ({Lexing.pos_fname = !f; Lexing.pos_lnum = !li;
+      Lexing.pos_bol = 0; Lexing.pos_cnum = !b},
+     {Lexing.pos_fname = !f; Lexing.pos_lnum = !li;
+      Lexing.pos_bol = 0; Lexing.pos_cnum = !e})
+  in
+  create_ident nm (User loc) l
+
 let id_derive ?(labels = []) nm id = create_ident nm (Derived id) labels
 
 let id_clone ?(labels = []) id =

src/ide/gconfig.ml

@@ -359,7 +359,7 @@ let preferences c =
   in
   (* editor *)
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
- let _ = GMisc.label ~text:"Default editor" ~packing:hb#add () in
+ let _ = GMisc.label ~text:"Default editor: " ~packing:(hb#pack ~expand:false) () in
  let editor_entry = GEdit.entry ~text:c.default_editor ~packing:hb#add () in
  let (_ : GtkSignal.id) =
     editor_entry#connect#changed ~callback:
@@ -378,7 +378,7 @@ let preferences c =
 *)
   (* timelimit ? *)
   let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
-  let _ = GMisc.label ~text:"Time limit" ~packing:hb#add () in
+  let _ = GMisc.label ~text:"Time limit: " ~packing:(hb#pack ~expand:false) () in
   let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
   timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. ();
   timelimit_spin#adjustment#set_value (float_of_int c.time_limit);
@@ -388,7 +388,7 @@ let preferences c =
   in
   (* nb of processes ? *)
   let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
-  let _ = GMisc.label ~text:"Nb of processes" ~packing:hb#add () in
+  let _ = GMisc.label ~text:"Nb of processes: " ~packing:(hb#pack ~expand:false) () in
   let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
   nb_processes_spin#adjustment#set_bounds
     ~lower:1. ~upper:16. ~step_incr:1. ();

src/ide/gmain.ml

@@ -1661,11 +1661,24 @@ let (_ : GMenu.image_menu_item) =
 (* vertical paned on the right*)
 (******************************)
 
+let right_vb = GPack.vbox ~packing:hp#add ()
+
 let vp =
   try
-    GPack.paned `VERTICAL ~packing:hp#add ()
+    GPack.paned `VERTICAL ~packing:right_vb#add ()
   with Gtk.Error _ -> assert false
 
+let right_hb = GPack.hbox ~packing:(right_vb#pack ~expand:false) ()
+
+let file_info = GMisc.label ~text:""
+  ~packing:(right_hb#pack ~fill:true) ()
+
+let current_file = ref ""
+
+let set_current_file f =
+  current_file := f;
+  file_info#set_text ("file: " ^ !current_file)
+
 (******************)
 (* goal text view *)
 (******************)
@@ -1714,8 +1727,6 @@ let source_view =
     ~packing:scrolled_source_view#add
     ()
 
-let current_file = ref ""
-
 (*
   source_view#misc#modify_font_by_name font_name;
 *)
@@ -1754,7 +1765,7 @@ let scroll_to_id id =
         if f <> !current_file then
           begin
             source_view#source_buffer#set_text (source_text f);
-            current_file := f;
+            set_current_file f;
           end;
         move_to_line source_view (l-1);
         erase_color_loc source_view;
@@ -1762,11 +1773,11 @@ let scroll_to_id id =
     | Ident.Fresh ->
         source_view#source_buffer#set_text
           "Fresh ident (no position available)\n";
-        current_file := ""
+        set_current_file ""
     | Ident.Derived _ ->
         source_view#source_buffer#set_text
           "Derived ident (no position available)\n";
-        current_file := ""
+        set_current_file ""
 
 let color_label = function
   | _, Some loc when (fst loc).Lexing.pos_fname = !current_file ->