Merge branch 'trunk' into located_switch

19 files changed, 251 insertions, 250 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 3a1d87787..cd45e2fcd 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -519,6 +519,7 @@ struct
   let all_basic = ["Printing"; "All"]
   let existential = ["Printing"; "Existential"; "Instances"]
   let universes = ["Printing"; "Universes"]
+  let unfocused = ["Printing"; "Unfocused"]
 
   type bool_descr = { opts : t list; init : bool; label : string }
 
@@ -534,7 +535,8 @@ struct
       label = "Display _existential variable instances" };
     { opts = [universes]; init = false; label = "Display _universe levels" };
     { opts = [all_basic;existential;universes]; init = false;
-      label = "Display all _low-level contents" }
+      label = "Display all _low-level contents" };
+    { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
   ]
 
   (** The current status of the boolean options *)
@@ -549,6 +551,8 @@ struct
 
   let _ = reset ()
 
+  let printing_unfocused () = Hashtbl.find current_state unfocused
+
   (** Transmitting options to coqtop *)
 
   let enforce h k =
diff --git a/ide/coq.mli b/ide/coq.mli
index ab8c12a6f..e8e2f5239 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -140,6 +140,8 @@ sig
 
   val set : t -> bool -> unit
 
+  val printing_unfocused: unit -> bool
+
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 50d0dc491..d30d7ab5e 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -117,7 +117,7 @@ end = struct
       (b#get_iter_at_mark s.start)#offset
       (b#get_iter_at_mark s.stop)#offset
       (ellipsize
-        ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
+        ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop)))
       (String.concat "," (List.map str_of_flag s.flags))
       (ellipsize
         (String.concat ","
@@ -128,9 +128,6 @@ end = struct
 end
 open SentenceId
 
-let log_pp msg : unit task =
-  Coq.lift (fun () -> Minilib.log_pp msg)
-
 let log msg : unit task =
   Coq.lift (fun () -> Minilib.log msg)
 
@@ -207,7 +204,7 @@ object (self)
     in
     List.iter (fun s -> set_index s (s.index + 1)) after;
     set_index s (document_length - List.length after);
-    ignore ((SentenceId.connect s)#changed self#on_changed);
+    ignore ((SentenceId.connect s)#changed ~callback:self#on_changed);
     document_length <- document_length + 1;
     List.iter (fun f -> f `INSERT) cbs
 
@@ -221,8 +218,8 @@ object (self)
     List.iter (fun f -> f `REMOVE) cbs
 
   initializer
-    let _ = (Doc.connect doc)#pushed self#on_push in
-    let _ = (Doc.connect doc)#popped self#on_pop in
+    let _ = (Doc.connect doc)#pushed ~callback:self#on_push in
+    let _ = (Doc.connect doc)#popped ~callback:self#on_pop in
     ()
 
 end
@@ -273,15 +270,15 @@ object(self)
         else iter
       in
       let iter = sentence_start iter in
-      script#buffer#place_cursor iter;
+      script#buffer#place_cursor ~where:iter;
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
-    let _ = segment#connect#clicked on_click in
+    let _ = segment#connect#clicked ~callback:on_click in
     ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
-    let x, y = script#window_to_buffer_coords `WIDGET x y in
-    let iter = script#get_iter_at_location x y in
+    let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+    let iter = script#get_iter_at_location ~x ~y in
     if iter#has_tag Tags.Script.tooltip then begin
       let s =
         let rec aux iter =
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index d55e7f9dd..5912bec35 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -105,8 +105,7 @@ let commands = [
    "Reset Extraction Inline";
    "Restore State";
    ];
-  [  "Save.";
-     "Scheme";
+  [  "Scheme";
      "Section";
      "Set Extraction AutoInline";
      "Set Extraction Optimize";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 25858acce..663e28d36 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -792,11 +792,11 @@ let coqtop_arguments sn =
         sn.messages#push Feedback.Error (Pp.str msg)
     else dialog#destroy ()
   in
-  let _ = entry#connect#activate ok_cb in
-  let _ = ok#connect#clicked ok_cb in
+  let _ = entry#connect#activate ~callback:ok_cb in
+  let _ = ok#connect#clicked ~callback:ok_cb in
   let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in
   let cancel_cb () = dialog#destroy () in
-  let _ = cancel#connect#clicked cancel_cb in
+  let _ = cancel#connect#clicked ~callback:cancel_cb in
   dialog#show ()
 
 let coqtop_arguments = cb_on_current_term coqtop_arguments
@@ -1103,8 +1103,8 @@ let build_ui () =
 
   menu templates_menu [
     item "Templates" ~label:"Te_mplates";
-    template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J");
-    template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T");
+    template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J");
+    template_item ("Theorem new_theorem : .\nProof.\n\nQed.\n", 8,11, "T");
     template_item ("Definition ident := .\n", 11,5, "E");
     template_item ("Inductive ident : :=\n  | : .\n", 10,5, "I");
     template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F");
@@ -1274,8 +1274,8 @@ let build_ui () =
     if b then toolbar#misc#show () else toolbar#misc#hide ()
   in
   stick show_toolbar toolbar refresh_toolbar;
-  let _ = source_style#connect#changed refresh_style in
-  let _ = source_language#connect#changed refresh_language in
+  let _ = source_style#connect#changed ~callback:refresh_style in
+  let _ = source_language#connect#changed ~callback:refresh_language in
 
   (* Color configuration *)
   Tags.Script.incomplete#set_property
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 2ae18593a..717c4000f 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -28,148 +28,149 @@ let list_queries menu li =
   res_buf
 
 let init () =
-  let theui = Printf.sprintf "<ui>
-<menubar name='CoqIde MenuBar'>
-  <menu action='File'>
-    <menuitem action='New' />
-    <menuitem action='Open' />
-    <menuitem action='Save' />
-    <menuitem action='Save as' />
-    <menuitem action='Save all' />
-    <menuitem action='Revert all buffers' />
-    <menuitem action='Close buffer' />
-    <menuitem action='Print...' />
-    <menu action='Export to'>
-      <menuitem action='Html' />
-      <menuitem action='Latex' />
-      <menuitem action='Dvi' />
-      <menuitem action='Pdf' />
-      <menuitem action='Ps' />
-    </menu>
-    <menuitem action='Rehighlight' />
-    %s
-  </menu>
-  <menu name='Edit' action='Edit'>
-    <menuitem action='Undo' />
-    <menuitem action='Redo' />
-    <separator />
-    <menuitem action='Cut' />
-    <menuitem action='Copy' />
-    <menuitem action='Paste' />
-    <separator />
-    <menuitem action='Find' />
-    <menuitem action='Find Next' />
-    <menuitem action='Find Previous' />
-    <menuitem action='Complete Word' />
-    <separator />
-    <menuitem action='External editor' />
-    <separator />
-    <menuitem name='Prefs' action='Preferences' />
-  </menu>
-  <menu name='View' action='View'>
-    <menuitem action='Previous tab' />
-    <menuitem action='Next tab' />
-    <separator/>
-    <menuitem action='Zoom in' />
-    <menuitem action='Zoom out' />
-    <menuitem action='Zoom fit' />
-    <separator/>
-    <menuitem action='Show Toolbar' />
-    <menuitem action='Query Pane' />
-    <separator/>
-    <menuitem action='Display implicit arguments' />
-    <menuitem action='Display coercions' />
-    <menuitem action='Display raw matching expressions' />
-    <menuitem action='Display notations' />
-    <menuitem action='Display all basic low-level contents' />
-    <menuitem action='Display existential variable instances' />
-    <menuitem action='Display universe levels' />
-    <menuitem action='Display all low-level contents' />
-  </menu>
-  <menu action='Navigation'>
-    <menuitem action='Forward' />
-    <menuitem action='Backward' />
-    <menuitem action='Go to' />
-    <menuitem action='Start' />
-    <menuitem action='End' />
-    <menuitem action='Interrupt' />
-    <menuitem action='Previous' />
-    <menuitem action='Next' />
-  </menu>
-  <menu action='Try Tactics'>
-    <menuitem action='auto' />
-    <menuitem action='auto with *' />
-    <menuitem action='eauto' />
-    <menuitem action='eauto with *' />
-    <menuitem action='intuition' />
-    <menuitem action='omega' />
-    <menuitem action='simpl' />
-    <menuitem action='tauto' />
-    <menuitem action='trivial' />
-    <menuitem action='Wizard' />
-    <separator />
-    %s
-  </menu>
-  <menu action='Templates'>
-    <menuitem action='Lemma' />
-    <menuitem action='Theorem' />
-    <menuitem action='Definition' />
-    <menuitem action='Inductive' />
-    <menuitem action='Fixpoint' />
-    <menuitem action='Scheme' />
-    <menuitem action='match' />
-    <separator />
-    %s
-  </menu>
-  <menu action='Queries'>
-    <menuitem action='Search' />
-    <menuitem action='Check' />
-    <menuitem action='Print' />
-    <menuitem action='About' />
-    <menuitem action='Locate' />
-    <menuitem action='Print Assumptions' />
-    <separator />
-    %s
-  </menu>
-  <menu name='Tools' action='Tools'>
-    <menuitem action='Comment' />
-    <menuitem action='Uncomment' />
-    <separator />
-    <menuitem action='Coqtop arguments' />
-  </menu>
-  <menu action='Compile'>
-    <menuitem action='Compile buffer' />
-    <menuitem action='Make' />
-    <menuitem action='Next error' />
-    <menuitem action='Make makefile' />
-  </menu>
-  <menu action='Windows'>
-    <menuitem action='Detach View' />
-  </menu>
-  <menu name='Help' action='Help'>
-    <menuitem action='Browse Coq Manual' />
-    <menuitem action='Browse Coq Library' />
-    <menuitem action='Help for keyword' />
-    <menuitem action='Help for μPG mode' />
-    <separator />
-    <menuitem name='Abt' action='About Coq' />
-  </menu>
-</menubar>
-<toolbar name='CoqIde ToolBar'>
-  <toolitem action='Save' />
-  <toolitem action='Close buffer' />
-  <toolitem action='Forward' />
-  <toolitem action='Backward' />
-  <toolitem action='Go to' />
-  <toolitem action='Start' />
-  <toolitem action='End' />
-  <toolitem action='Force' />
-  <toolitem action='Interrupt' />
-  <toolitem action='Previous' />
-  <toolitem action='Next' />
-  <toolitem action='Wizard' />
-</toolbar>
-</ui>"
+  let theui = Printf.sprintf "<ui>\
+\n<menubar name='CoqIde MenuBar'>\
+\n  <menu action='File'>\
+\n    <menuitem action='New' />\
+\n    <menuitem action='Open' />\
+\n    <menuitem action='Save' />\
+\n    <menuitem action='Save as' />\
+\n    <menuitem action='Save all' />\
+\n    <menuitem action='Revert all buffers' />\
+\n    <menuitem action='Close buffer' />\
+\n    <menuitem action='Print...' />\
+\n    <menu action='Export to'>\
+\n      <menuitem action='Html' />\
+\n      <menuitem action='Latex' />\
+\n      <menuitem action='Dvi' />\
+\n      <menuitem action='Pdf' />\
+\n      <menuitem action='Ps' />\
+\n    </menu>\
+\n    <menuitem action='Rehighlight' />\
+\n    %s\
+\n  </menu>\
+\n  <menu name='Edit' action='Edit'>\
+\n    <menuitem action='Undo' />\
+\n    <menuitem action='Redo' />\
+\n    <separator />\
+\n    <menuitem action='Cut' />\
+\n    <menuitem action='Copy' />\
+\n    <menuitem action='Paste' />\
+\n    <separator />\
+\n    <menuitem action='Find' />\
+\n    <menuitem action='Find Next' />\
+\n    <menuitem action='Find Previous' />\
+\n    <menuitem action='Complete Word' />\
+\n    <separator />\
+\n    <menuitem action='External editor' />\
+\n    <separator />\
+\n    <menuitem name='Prefs' action='Preferences' />\
+\n  </menu>\
+\n  <menu name='View' action='View'>\
+\n    <menuitem action='Previous tab' />\
+\n    <menuitem action='Next tab' />\
+\n    <separator/>\
+\n    <menuitem action='Zoom in' />\
+\n    <menuitem action='Zoom out' />\
+\n    <menuitem action='Zoom fit' />\
+\n    <separator/>\
+\n    <menuitem action='Show Toolbar' />\
+\n    <menuitem action='Query Pane' />\
+\n    <separator/>\
+\n    <menuitem action='Display implicit arguments' />\
+\n    <menuitem action='Display coercions' />\
+\n    <menuitem action='Display raw matching expressions' />\
+\n    <menuitem action='Display notations' />\
+\n    <menuitem action='Display all basic low-level contents' />\
+\n    <menuitem action='Display existential variable instances' />\
+\n    <menuitem action='Display universe levels' />\
+\n    <menuitem action='Display all low-level contents' />\
+\n    <menuitem action='Display unfocused goals' />\
+\n  </menu>\
+\n  <menu action='Navigation'>\
+\n    <menuitem action='Forward' />\
+\n    <menuitem action='Backward' />\
+\n    <menuitem action='Go to' />\
+\n    <menuitem action='Start' />\
+\n    <menuitem action='End' />\
+\n    <menuitem action='Interrupt' />\
+\n    <menuitem action='Previous' />\
+\n    <menuitem action='Next' />\
+\n  </menu>\
+\n  <menu action='Try Tactics'>\
+\n    <menuitem action='auto' />\
+\n    <menuitem action='auto with *' />\
+\n    <menuitem action='eauto' />\
+\n    <menuitem action='eauto with *' />\
+\n    <menuitem action='intuition' />\
+\n    <menuitem action='omega' />\
+\n    <menuitem action='simpl' />\
+\n    <menuitem action='tauto' />\
+\n    <menuitem action='trivial' />\
+\n    <menuitem action='Wizard' />\
+\n    <separator />\
+\n    %s\
+\n  </menu>\
+\n  <menu action='Templates'>\
+\n    <menuitem action='Lemma' />\
+\n    <menuitem action='Theorem' />\
+\n    <menuitem action='Definition' />\
+\n    <menuitem action='Inductive' />\
+\n    <menuitem action='Fixpoint' />\
+\n    <menuitem action='Scheme' />\
+\n    <menuitem action='match' />\
+\n    <separator />\
+\n    %s\
+\n  </menu>\
+\n  <menu action='Queries'>\
+\n    <menuitem action='Search' />\
+\n    <menuitem action='Check' />\
+\n    <menuitem action='Print' />\
+\n    <menuitem action='About' />\
+\n    <menuitem action='Locate' />\
+\n    <menuitem action='Print Assumptions' />\
+\n    <separator />\
+\n    %s\
+\n  </menu>\
+\n  <menu name='Tools' action='Tools'>\
+\n    <menuitem action='Comment' />\
+\n    <menuitem action='Uncomment' />\
+\n    <separator />\
+\n    <menuitem action='Coqtop arguments' />\
+\n  </menu>\
+\n  <menu action='Compile'>\
+\n    <menuitem action='Compile buffer' />\
+\n    <menuitem action='Make' />\
+\n    <menuitem action='Next error' />\
+\n    <menuitem action='Make makefile' />\
+\n  </menu>\
+\n  <menu action='Windows'>\
+\n    <menuitem action='Detach View' />\
+\n  </menu>\
+\n  <menu name='Help' action='Help'>\
+\n    <menuitem action='Browse Coq Manual' />\
+\n    <menuitem action='Browse Coq Library' />\
+\n    <menuitem action='Help for keyword' />\
+\n    <menuitem action='Help for μPG mode' />\
+\n    <separator />\
+\n    <menuitem name='Abt' action='About Coq' />\
+\n  </menu>\
+\n</menubar>\
+\n<toolbar name='CoqIde ToolBar'>\
+\n  <toolitem action='Save' />\
+\n  <toolitem action='Close buffer' />\
+\n  <toolitem action='Forward' />\
+\n  <toolitem action='Backward' />\
+\n  <toolitem action='Go to' />\
+\n  <toolitem action='Start' />\
+\n  <toolitem action='End' />\
+\n  <toolitem action='Force' />\
+\n  <toolitem action='Interrupt' />\
+\n  <toolitem action='Previous' />\
+\n  <toolitem action='Next' />\
+\n  <toolitem action='Wizard' />\
+\n</toolbar>\
+\n</ui>"
     (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
     (Buffer.contents (list_items "Tactic" Coq_commands.tactics))
     (Buffer.contents (list_items "Template" Coq_commands.commands))
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index 043ad6008..df988d8f1 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -4,6 +4,5 @@ Xml_printer
 Serialize
 Richpp
 Xmlprotocol
-Texmacspp
 Document
 Ide_slave
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bbc3e4bcb..ac7b38681 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -54,7 +54,8 @@ let coqide_known_option table = List.mem table [
   ["Printing";"All"];
   ["Printing";"Records"];
   ["Printing";"Existential";"Instances"];
-  ["Printing";"Universes"]]
+  ["Printing";"Universes"];
+  ["Printing";"Unfocused"]]
 
 let is_known_option cmd = match cmd with
   | VernacSetOption (o,BoolValue true)
@@ -82,7 +83,7 @@ let add ((s,eid),(sid,verbose)) =
   let loc_ast = Stm.parse_sentence sid pa in
   let newid, rc = Stm.add ~ontop:sid verbose loc_ast in
   let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  ide_cmd_checks newid loc_ast;
+  ide_cmd_checks ~id:newid loc_ast;
   (* TODO: the "" parameter is a leftover of the times the protocol
    * used to include stderr/stdout output.
    *
@@ -387,14 +388,8 @@ let interp ((_raw, verbose), s) =
 
 let quit = ref false
 
-(** Serializes the output of Stm.get_ast  *)
-let print_ast id =
-  match Stm.get_ast id with
-  | Some (loc, expr) -> begin
-      try  Texmacspp.tmpp ?loc expr
-      with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
-    end
-  | None     -> Xml_datatype.PCData "ERROR"
+(** Disabled *)
+let print_ast id = Xml_datatype.PCData "ERROR"
 
 (** Grouping all call handlers together + error handling *)
 
@@ -505,12 +500,12 @@ let rec parse = function
 
 let () = Coqtop.toploop_init := (fun args ->
         let args = parse args in
-        Flags.make_silent true;
+        Flags.quiet := true;
         CoqworkmgrApi.(init Flags.High);
         args)
 
 let () = Coqtop.toploop_run := loop
 
 let () = Usage.add_to_usage "coqidetop"
-"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format
-  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
+"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
+\n  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index da867e689..a08ab07b5 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -35,17 +35,6 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
-let xml_to_string xml =
-  let open Xml_datatype in
-  let buf = Buffer.create 1024 in
-  let rec iter = function
-  | PCData s -> Buffer.add_string buf s
-  | Element (_, _, children) ->
-    List.iter iter children
-  in
-  let () = iter xml in
-  Buffer.contents buf
-
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
   (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
       it has to reimplement its own helper function. Unluckily, it relies on
@@ -58,7 +47,7 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
     let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in
     let start = buf#get_iter_at_mark mark in
     let stop = buf#get_iter_at_mark rmark in
-    let iter tag = buf#apply_tag tag start stop in
+    let iter tag = buf#apply_tag tag ~start ~stop in
     List.iter iter tags
 
 let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
diff --git a/ide/preferences.ml b/ide/preferences.ml
index f0fd45d77..9fe9c6337 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -73,8 +73,8 @@ end
 let stick (pref : 'a preference) (obj : #GObj.widget as 'obj)
   (cb : 'a -> unit) =
   let _ = cb pref#get in
-  let p_id = pref#connect#changed (fun v -> cb v) in
-  let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in
+  let p_id = pref#connect#changed ~callback:(fun v -> cb v) in
+  let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in
   ()
 
 (** Useful marshallers *)
@@ -314,7 +314,7 @@ let attach_modifiers (pref : string preference) prefix =
     in
     GtkData.AccelMap.foreach change
   in
-  pref#connect#changed cb
+  pref#connect#changed ~callback:cb
 
 let modifier_for_navigation =
   new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)
@@ -360,7 +360,7 @@ object
     ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
     as super
 
-  method set v =
+  method! set v =
     if not (Flags.is_standard_doc_url v) &&
       v <> use_default_doc_url &&
       (* Extra hack to support links to last released doc version *)
@@ -408,10 +408,10 @@ let background_color =
   new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)
 
 let attach_bg (pref : string preference) (tag : GText.tag) =
-  pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c))
+  pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c))
 
 let attach_fg (pref : string preference) (tag : GText.tag) =
-  pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c))
+  pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c))
 
 let processing_color =
   new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
@@ -468,7 +468,7 @@ let create_tag name default =
   let iter table =
     let tag = GText.tag ~name () in
     table#add tag#as_tag;
-    ignore (pref#connect#changed (fun _ -> set_tag tag));
+    ignore (pref#connect#changed ~callback:(fun _ -> set_tag tag));
     set_tag tag;
   in
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
@@ -601,8 +601,8 @@ object (self)
     box#pack italic#coerce;
     box#pack underline#coerce;
     let cb but obj = obj#set_sensitive (not but#active) in
-    let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in
-    let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in
+    let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
+    let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
     ()
 
 end
@@ -692,7 +692,7 @@ let configure ?(apply=(fun () -> ())) () =
         ~color:(Tags.color_of_string pref#get)
         ~packing:(table#attach ~left:1 ~top:i) ()
       in
-      let _ = button#connect#color_set begin fun () ->
+      let _ = button#connect#color_set ~callback:begin fun () ->
         pref#set (Tags.string_of_color button#color)
       end in
       let reset _ =
@@ -754,7 +754,7 @@ let configure ?(apply=(fun () -> ())) () =
     let button text (pref : bool preference) =
       let active = pref#get in
       let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
-      ignore (but#connect#toggled (fun () -> pref#set but#active))
+      ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active))
     in
     let () = button "Dynamic word wrap" dynamic_word_wrap in
     let () = button "Show line number" show_line_number in
diff --git a/ide/session.ml b/ide/session.ml
index 6262820e7..7aea75ac8 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -249,8 +249,8 @@ let make_table_widget ?sort cd cb =
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true in
   let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed refresh in
-  let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in
+  let _ = background_color#connect#changed ~callback:refresh in
+  let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -308,8 +308,8 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
         !callback errs;
 	List.iter (fun (lno, msg) -> access (fun columns store ->
           let line = store#append () in
-          store#set line (find_int_col "Line" columns) lno;
-          store#set line (find_string_col "Error message" columns) msg))
+          store#set ~row:line ~column:(find_int_col "Line" columns) lno;
+          store#set ~row:line ~column:(find_string_col "Error message" columns) msg))
           errs
       end
     method on_update ~callback:cb = callback := cb
@@ -348,8 +348,8 @@ let create_jobpage coqtop coqops : jobpage =
               else false)
           else
             let line = store#append () in
-            store#set line column id;
-            store#set line (find_string_col "Job name" columns) job))
+            store#set ~row:line ~column id;
+            store#set ~row:line ~column:(find_string_col "Job name" columns) job))
           jobs
       end
     method on_update ~callback:cb = callback := cb
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 3fcb7ce49..621c46b94 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -91,8 +91,8 @@ object(self)
     let result = GText.view ~packing:r_bin#add () in
     views <- (frame#coerce, result, combo#entry) :: views;
     let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
-    let _ = background_color#connect#changed cb in
-    let _ = result#misc#connect#realize (fun () -> cb background_color#get) in
+    let _ = background_color#connect#changed ~callback:cb in
+    let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
     let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
     stick text_font result cb;
     result#misc#set_can_focus true; (* false causes problems for selection *)
@@ -165,7 +165,7 @@ object(self)
     self#new_page_maker;
     self#new_query_aux ~grab_now:false ();
     frame#misc#hide ();
-    let _ = background_color#connect#changed self#refresh_color in
+    let _ = background_color#connect#changed ~callback:self#refresh_color in
     self#refresh_color background_color#get;
     ignore(notebook#event#connect#key_press ~callback:(fun ev ->
       if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true)
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index aeae3e1fd..3bb6b780e 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -154,7 +154,7 @@ object (self)
     let () = store#clear () in
     let iter prop =
       let iter = store#append () in
-      store#set iter column prop
+      store#set ~row:iter ~column prop
     in
     let () = current_completion <- (pref, props) in
     Proposals.iter iter props
@@ -267,7 +267,7 @@ object (self)
     (** Position of view w.r.t. window *)
     let (ux, uy) = Gdk.Window.get_position view#misc#window in
     (** Relative buffer position to view *)
-    let (dx, dy) = view#window_to_buffer_coords `WIDGET 0 0 in
+    let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in
     (** Iter position *)
     let iter = view#buffer#get_iter pos in
     let coords = view#get_iter_location iter in
@@ -397,11 +397,11 @@ object (self)
     let () = self#select_first () in
     let () = obj#misc#show () in
     let () = self#manage_scrollbar () in
-    obj#resize 1 1
+    obj#resize ~width:1 ~height:1
 
   method private start_callback off =
     let (x, y, w, h) = self#coordinates (`OFFSET off) in
-    let () = obj#move x (y + 3 * h / 2) in
+    let () = obj#move ~x ~y:(y + 3 * h / 2) in
     ()
 
   method private update_callback (off, word, props) =
@@ -433,21 +433,21 @@ object (self)
       else false
     in
     (** Style handling *)
-    let _ = view#misc#connect#style_set self#refresh_style in
+    let _ = view#misc#connect#style_set ~callback:self#refresh_style in
     let _ = self#refresh_style () in
     let _ = data#set_resize_mode `PARENT in
     let _ = frame#set_resize_mode `PARENT in
     (** Callback to model *)
-    let _ = model#connect#start_completion self#start_callback in
-    let _ = model#connect#update_completion self#update_callback in
-    let _ = model#connect#end_completion self#end_callback in
+    let _ = model#connect#start_completion ~callback:self#start_callback in
+    let _ = model#connect#update_completion ~callback:self#update_callback in
+    let _ = model#connect#end_completion ~callback:self#end_callback in
     (** Popup interaction *)
-    let _ = view#event#connect#key_press key_cb in
+    let _ = view#event#connect#key_press ~callback:key_cb in
     (** Hiding the popup when necessary*)
-    let _ = view#misc#connect#hide obj#misc#hide in
-    let _ = view#event#connect#button_press (fun _ -> self#hide (); false) in
-    let _ = view#connect#move_cursor move_cb in
-    let _ = view#event#connect#focus_out (fun _ -> self#hide (); false) in
+    let _ = view#misc#connect#hide ~callback:obj#misc#hide in
+    let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in
+    let _ = view#connect#move_cursor ~callback:move_cb in
+    let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in
     ()
 
 end
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index 3d1b63dfa..cbc34462e 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -26,8 +26,8 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
     val mutable attached_cb = (fun _ -> ())
 
     method child = frame#child
-    method add = frame#add
-    method pack ?from ?expand ?fill ?padding w =
+    method! add = frame#add
+    method! pack ?from ?expand ?fill ?padding w =
       if frame#all_children = [] then self#add w
       else raise (Invalid_argument "detachable#pack")
 
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 3d847ddcc..f84b9063b 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -186,8 +186,8 @@ class finder name (view : GText.view) =
       in
       let find_cb = generic_cb self#hide self#find_forward in
       let replace_cb = generic_cb self#hide self#replace in
-      let _ = find_entry#event#connect#key_press find_cb in
-      let _ = replace_entry#event#connect#key_press replace_cb in
+      let _ = find_entry#event#connect#key_press ~callback:find_cb in
+      let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
 
       (** TextView interaction *)
       let view_cb ev =
@@ -197,7 +197,7 @@ class finder name (view : GText.view) =
           else false
         else false
       in
-      let _ = view#event#connect#key_press view_cb in
+      let _ = view#event#connect#key_press ~callback:view_cb in
       ()
 
   end
diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml
index 08d7d1983..0e5284c2f 100644
--- a/ide/wg_Notebook.ml
+++ b/ide/wg_Notebook.ml
@@ -50,7 +50,7 @@ object(self)
 
   method pages = term_list
 
-  method remove_page index =
+  method! remove_page index =
     term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list;
     super#remove_page index
 
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 3cbe58388..0bf5afbfd 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -47,7 +47,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
                      hover_cb start stop; false
                  | _ -> false))
 
-let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
+let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with
   | [] -> assert false
   | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
       let on_hover sel_start sel_stop =
@@ -65,8 +65,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       let head_str = Printf.sprintf
         "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
       in
-      let goal_str index total = Printf.sprintf
-        "______________________________________(%d/%d)\n" index total
+      let goal_str ?(shownum=false) index total =
+        if shownum then Printf.sprintf
+                          "______________________________________(%d/%d)\n" index total
+        else Printf.sprintf
+               "______________________________________\n"
       in
       (* Insert current goal and its hypotheses *)
       let hyps_hints, goal_hints = match hints with
@@ -97,18 +100,29 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           [tag]
           else []
         in
-        proof#buffer#insert (goal_str 1 goals_cnt);
+        proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
         insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
-      let fold_goal i _ { Interface.goal_ccl = g } =
-        proof#buffer#insert (goal_str i goals_cnt);
+      let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } =
+        proof#buffer#insert (goal_str ~shownum i goals_cnt);
         insert_xml proof#buffer (Richpp.richpp_of_pp width g);
         proof#buffer#insert "\n"
       in
-      let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
-
+      let () = Util.List.fold_left_i (fold_goal ~shownum:true) 2 () rem_goals in
+      (* show unfocused goal if option set *)
+      (* Insert remaining goals (no hypotheses) *)
+      if Coq.PrintOpt.printing_unfocused () then
+        begin
+          ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter));
+          let unfoc = List.flatten (List.rev (List.map (fun (x,y) -> x@y) unfoc_goals)) in
+          if unfoc<>[] then
+            begin
+              proof#buffer#insert "\nUnfocused Goals:\n";
+              Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc
+            end
+        end;
       ignore(proof#buffer#place_cursor
                ~where:(proof#buffer#end_iter#backward_to_tag_toggle
                          (Some Tags.Proof.goal)));
@@ -172,8 +186,9 @@ let display mode (view : #GText.view_skel) goals hints evars =
       in
       List.iteri iter bg
     end
-  | Some { Interface.fg_goals = fg } ->
-    mode view fg hints
+  | Some { Interface.fg_goals = fg; bg_goals = bg } ->
+    mode view fg ~unfoc_goals:bg hints
+
 
 let proof_view () =
   let buffer = GSourceView2.source_buffer
@@ -188,8 +203,8 @@ let proof_view () =
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed cb in
-  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let _ = background_color#connect#changed ~callback:cb in
+  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
 
@@ -226,5 +241,5 @@ let proof_view () =
   (* Is there a better way to connect the signal ? *)
   (* Can this be done in the object constructor? *)
   let w_cb _ = pf#refresh ~force:false in
-  ignore (view#misc#connect#size_allocate w_cb);
+  ignore (view#misc#connect#size_allocate ~callback:w_cb);
   pf
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 218cedb36..7430f07d4 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -301,28 +301,28 @@ object (self)
       ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
 
   (* HACK: missing gtksourceview features *)
-  method right_margin_position =
+  method! right_margin_position =
     let prop = {
       Gobject.name = "right-margin-position";
       conv = Gobject.Data.int;
     } in
     Gobject.get prop obj
 
-  method set_right_margin_position pos =
+  method! set_right_margin_position pos =
     let prop = {
       Gobject.name = "right-margin-position";
       conv = Gobject.Data.int;
     } in
     Gobject.set prop obj pos
 
-  method show_right_margin =
+  method! show_right_margin =
     let prop = {
       Gobject.name = "show-right-margin";
       conv = Gobject.Data.boolean;
     } in
     Gobject.get prop obj
 
-  method set_show_right_margin show =
+  method! set_show_right_margin show =
     let prop = {
       Gobject.name = "show-right-margin";
       conv = Gobject.Data.boolean;
@@ -460,8 +460,8 @@ object (self)
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
     (** Plug on preferences *)
     let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
-    let _ = background_color#connect#changed cb in
-    let _ = self#misc#connect#realize (fun () -> cb background_color#get) in
+    let _ = background_color#connect#changed ~callback:cb in
+    let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
 
     let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in
     stick dynamic_word_wrap self cb;
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index dbc1740ef..d527a0d13 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -75,7 +75,7 @@ object (self)
         self#redraw ();
       end
     in
-    let _ = box#misc#connect#size_allocate cb in
+    let _ = box#misc#connect#size_allocate ~callback:cb in
     let clicked_cb ev = match model with
     | None -> true
     | Some md ->
@@ -86,7 +86,7 @@ object (self)
       let () = clicked#call idx in
       true
     in
-    let _ = eventbox#event#connect#button_press clicked_cb in
+    let _ = eventbox#event#connect#button_press ~callback:clicked_cb in
     let cb show = if show then self#misc#show () else self#misc#hide () in
     stick show_progress_bar self cb;
     (** Initial pixmap *)
@@ -102,7 +102,7 @@ object (self)
     | `SET (i, color) ->
       if self#misc#visible then self#fill_range color i (i + 1)
     in
-    md#changed changed_cb
+    md#changed ~callback:changed_cb
 
   method private fill_range color i j = match model with
   | None -> ()