Imported Upstream version 8.9.0upstream/8.9.0upstream

39 files changed, 220 insertions, 120 deletions

diff --git a/ide/.merlin b/ide/.merlin.in
index 953b5dce..4dc6f455 100644
--- a/ide/.merlin
+++ b/ide/.merlin.in
@@ -2,5 +2,7 @@ PKG unix laglgtk2 lablgtk2.sourceview2
 
 S utils
 B utils
+S protocol
+B protocol
 
 REC
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 47612cdf..54a592a0 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -217,7 +217,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Load" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fourier" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
diff --git a/ide/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh
deleted file mode 100755
index a24af939..00000000
--- a/ide/MacOS/relatify_with-respect-to_.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/sh
-
-set -e
-
-for i in "$3/"*.dylib
-do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1"
-done
-case "$1" in
-	*.dylib)
-	    install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1
-	    for i in "$3"/*.dylib
-	    do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i
-	    done;;
-	*)
-esac
diff --git a/ide/utils/configwin.ml b/ide/configwin.ml
index 69e8b647..69e8b647 100644
--- a/ide/utils/configwin.ml
+++ b/ide/configwin.ml
diff --git a/ide/utils/configwin.mli b/ide/configwin.mli
index 7616e471..7616e471 100644
--- a/ide/utils/configwin.mli
+++ b/ide/configwin.mli
diff --git a/ide/utils/configwin_ihm.ml b/ide/configwin_ihm.ml
index d16efa60..d16efa60 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
diff --git a/ide/utils/configwin_ihm.mli b/ide/configwin_ihm.mli
index c867ad91..c867ad91 100644
--- a/ide/utils/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
diff --git a/ide/utils/configwin_messages.ml b/ide/configwin_messages.ml
index de1b4721..de1b4721 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/configwin_messages.ml
diff --git a/ide/utils/configwin_types.mli b/ide/configwin_types.ml
index 9e339d13..9e339d13 100644
--- a/ide/utils/configwin_types.mli
+++ b/ide/configwin_types.ml
diff --git a/ide/coq.ml b/ide/coq.ml
index 65456d68..e9483601 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -152,7 +152,7 @@ let print_status = function
 let check_connection args =
   let lines = ref [] in
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote (coqtop_path ()) ^ " -batch -ideslave " ^ argstr in
+  let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
   let cmd = requote cmd in
   try
     let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
@@ -377,7 +377,7 @@ let spawn_handle args respawner feedback_processor =
     else
       "on"
   in
-  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: args) in
   let env =
     match !ideslave_coqtop_flags with
     | None -> None
@@ -530,20 +530,31 @@ let break_coqtop coqtop workers =
 
 module PrintOpt =
 struct
-  type t = string list
+  type _ t =
+  | BoolOpt : string list -> bool t
+  | StringOpt : string list -> string t
+
+  let opt_name (type a) : a t -> string list = function
+  | BoolOpt l -> l
+  | StringOpt l -> l
+
+  let opt_data (type a) (key : a t) (v : a) = match key with
+  | BoolOpt l -> Interface.BoolValue v
+  | StringOpt l -> Interface.StringValue v
 
   (* Boolean options *)
 
-  let implicit = ["Printing"; "Implicit"]
-  let coercions = ["Printing"; "Coercions"]
-  let raw_matching = ["Printing"; "Matching"]
-  let notations = ["Printing"; "Notations"]
-  let all_basic = ["Printing"; "All"]
-  let existential = ["Printing"; "Existential"; "Instances"]
-  let universes = ["Printing"; "Universes"]
-  let unfocused = ["Printing"; "Unfocused"]
+  let implicit = BoolOpt ["Printing"; "Implicit"]
+  let coercions = BoolOpt ["Printing"; "Coercions"]
+  let raw_matching = BoolOpt ["Printing"; "Matching"]
+  let notations = BoolOpt ["Printing"; "Notations"]
+  let all_basic = BoolOpt ["Printing"; "All"]
+  let existential = BoolOpt ["Printing"; "Existential"; "Instances"]
+  let universes = BoolOpt ["Printing"; "Universes"]
+  let unfocused = BoolOpt ["Printing"; "Unfocused"]
+  let diff = StringOpt ["Diffs"]
 
-  type bool_descr = { opts : t list; init : bool; label : string }
+  type 'a descr = { opts : 'a t list; init : 'a; label : string }
 
   let bool_items = [
     { opts = [implicit]; init = false; label = "Display _implicit arguments" };
@@ -561,24 +572,32 @@ struct
     { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
   ]
 
+  let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" }
+
   (** The current status of the boolean options *)
 
   let current_state = Hashtbl.create 11
 
-  let set opt v = Hashtbl.replace current_state opt v
+  let set (type a) (opt : a t) (v : a) =
+    Hashtbl.replace current_state (opt_name opt) (opt_data opt v)
 
   let reset () =
     let init_descr d = List.iter (fun o -> set o d.init) d.opts in
-    List.iter init_descr bool_items
+    List.iter init_descr bool_items;
+    List.iter (fun o -> set o diff_item.init) diff_item.opts
 
   let _ = reset ()
 
-  let printing_unfocused () = Hashtbl.find current_state unfocused
+  let printing_unfocused () =
+  let BoolOpt unfocused = unfocused in
+  match Hashtbl.find current_state unfocused with
+  | Interface.BoolValue b -> b
+  | _ -> assert false
 
   (** Transmitting options to coqtop *)
 
   let enforce h k =
-    let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
+    let mkopt o v acc = (o, v) :: acc in
     let opts = Hashtbl.fold mkopt current_state [] in
     eval_call (Xmlprotocol.set_options opts) h
       (function
diff --git a/ide/coq.mli b/ide/coq.mli
index 40a6dea8..3af0aa69 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -134,13 +134,15 @@ val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
 
 module PrintOpt :
 sig
-  type t (** Representation of an option *)
+  type 'a t (** Representation of an option *)
 
-  type bool_descr = { opts : t list; init : bool; label : string }
+  type 'a descr = { opts : 'a t list; init : 'a; label : string }
 
-  val bool_items : bool_descr list
+  val bool_items : bool descr list
 
-  val set : t -> bool -> unit
+  val diff_item : string descr
+
+  val set : 'a t -> 'a -> unit
 
   val printing_unfocused: unit -> bool
 
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index f5dba208..b0bafb79 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -311,7 +311,6 @@ let tactics =
      "fix __ with";
      "fold";
      "fold __ in";
-     "fourier";
      "functional induction";
    ];
 
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 1fdd7317..b6654f6d 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -23,7 +23,11 @@ let number = [ '0'-'9' ]+
 
 let string = "\"" _+ "\""
 
-let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
+let alpha = ['a'-'z' 'A'-'Z']
+
+let ident = alpha (alpha | number | '_' | "'")*
+
+let undotted_sep = ((number | '[' ident ']') space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
 
 let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f5ff0899..a4d45c6d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -826,6 +826,7 @@ let refresh_notebook_pos () =
 
 let menu = GAction.add_actions
 let item = GAction.add_action
+let radio = GAction.add_radio_action
 
 (** Toggle items in menus for printing options *)
 
@@ -1003,8 +1004,6 @@ let build_ui () =
     item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP
       ~accel:"<Shift>F3"
       ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
-    item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
-      ~callback:(fun _ -> ());
     item "External editor" ~label:"External editor" ~stock:`EDIT
       ~callback:External.editor;
     item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
@@ -1043,7 +1042,27 @@ let build_ui () =
       ~callback:(fun _ -> show_toolbar#set (not show_toolbar#get));
     item "Query Pane" ~label:"_Query Pane"
       ~accel:"F1"
-      ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
+      ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane);
+    GAction.group_radio_actions
+      ~init_value:(
+        let v = diffs#get in
+        List.iter (fun o -> Opt.set o v) Opt.diff_item.Opt.opts;
+        if v = "on" then 1
+        else if v = "removed" then 2
+        else 0)
+      ~callback:begin fun n ->
+        (match n with
+        | 0 -> List.iter (fun o -> Opt.set o "off"; diffs#set "off") Opt.diff_item.Opt.opts
+        | 1 -> List.iter (fun o -> Opt.set o "on"; diffs#set "on") Opt.diff_item.Opt.opts
+        | 2 -> List.iter (fun o -> Opt.set o "removed"; diffs#set "removed") Opt.diff_item.Opt.opts
+        | _ -> assert false);
+        send_to_coq (fun sn -> sn.coqops#show_goals)
+        end
+      [
+        radio "Unset diff" 0 ~label:"_Don't show diffs";
+        radio "Set diff" 1 ~label:"Show diffs: only _added";
+        radio "Set removed diff" 2 ~label:"Show diffs: added and _removed";
+      ];
   ];
   toggle_items view_menu Coq.PrintOpt.bool_items;
 
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 717c4000..c994898a 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -60,7 +60,6 @@ let init () =
 \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 />\
@@ -86,6 +85,10 @@ let init () =
 \n    <menuitem action='Display universe levels' />\
 \n    <menuitem action='Display all low-level contents' />\
 \n    <menuitem action='Display unfocused goals' />\
+\n    <separator/>\
+\n    <menuitem action='Unset diff' />\
+\n    <menuitem action='Set diff' />\
+\n    <menuitem action='Set removed diff' />\
 \n  </menu>\
 \n  <menu action='Navigation'>\
 \n    <menuitem action='Forward' />\
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 9f5c9924..d554bebd 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -35,8 +35,11 @@ let find_word_start (it:GText.iter) =
       (Minilib.log "find_word_start: cannot backward"; it)
     else if is_word_char it#char
     then step_to_start it
-    else (it#nocopy#forward_char;
-	Minilib.log ("Word start at: "^(string_of_int it#offset));it)
+    else begin
+      ignore(it#nocopy#forward_char);
+      Minilib.log ("Word start at: "^(string_of_int it#offset));
+      it
+    end
   in
     step_to_start it#copy
 
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 96ea8c41..a7ade713 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,15 +9,7 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Serialize
-Richprinter
-Xml_lexer
-Xml_parser
-Xml_printer
-Serialize
-Richpp
 Topfmt
-Xmlprotocol
 Ideutils
 Coq
 Coq_lex
diff --git a/ide/coqidetop.mllib b/ide/ide_common.mllib
index df988d8f..050c282e 100644
--- a/ide/coqidetop.mllib
+++ b/ide/ide_common.mllib
@@ -5,4 +5,3 @@ Serialize
 Richpp
 Xmlprotocol
 Document
-Ide_slave
diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli
deleted file mode 100644
index 9db9ecd1..00000000
--- a/ide/ide_slave.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* This empty file avoids a race condition that occurs when compiling a .ml file
-   that does not have a corresponding .mli file *)
diff --git a/ide/ide_slave.ml b/ide/idetop.ml
index 6b7efc83..8a221a93 100644
--- a/ide/ide_slave.ml
+++ b/ide/idetop.ml
@@ -18,9 +18,8 @@ open Printer
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
-(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
-    function and a rewind function. This specialized loop is triggered
-    when the -ideslave option is passed to Coqtop. *)
+(** Idetop : an implementation of [Interface], i.e. mainly an interp
+    function and a rewind function. *)
 
 
 (** Signal handling: we postpone ^C during input and output phases,
@@ -54,10 +53,12 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Records"];
   ["Printing";"Existential";"Instances"];
   ["Printing";"Universes"];
-  ["Printing";"Unfocused"]]
+  ["Printing";"Unfocused"];
+  ["Diffs"]]
 
 let is_known_option cmd = match Vernacprop.under_control cmd with
   | VernacSetOption (_, o, BoolValue true)
+  | VernacSetOption (_, o, StringValue _)
   | VernacUnsetOption (_, o) -> coqide_known_option o
   | _ -> false
 
@@ -81,7 +82,7 @@ let set_doc doc = ide_doc := Some doc
 
 let add ((s,eid),(sid,verbose)) =
   let doc = get_doc () in
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let pa = Pcoq.Parsable.make (Stream.of_string s) in
   let loc_ast = Stm.parse_sentence ~doc sid pa in
   let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
   set_doc doc;
@@ -114,14 +115,14 @@ let edit_at id =
  * be removed in the next version of the protocol.
  *)
 let query (route, (s,id)) =
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let pa = Pcoq.Parsable.make (Stream.of_string s) in
   let doc = get_doc () in
   Stm.query ~at:id ~doc ~route pa
 
 let annotate phrase =
   let doc = get_doc () in
   let {CAst.loc;v=ast} =
-    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
+    let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
     Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
   in
   (* XXX: Width should be a parameter of annotate... *)
@@ -152,7 +153,7 @@ let hyp_next_tac sigma env decl =
     ("inversion clear "^id_s), ("inversion_clear "^id_s^".")
   ]
 
-let concl_next_tac sigma concl =
+let concl_next_tac =
   let expand s = (s,s^".") in
   List.map expand ([
     "intro";
@@ -207,9 +208,32 @@ let goals () =
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
-    let pfts = Proof_global.give_me_the_proof () in
-    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
-  with Proof_global.NoCurrentProof -> None
+    let newp = Proof_global.give_me_the_proof () in
+    if Proof_diffs.show_diffs () then begin
+      let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
+      let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
+      let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
+        try Evar.Map.find ng diff_goal_map  with Not_found -> ng
+      in
+
+      let process_goal_diffs nsigma ng =
+        let open Evd in
+        let og = map_goal_for_diff ng in
+        let og_s = match oldp with
+        | Some oldp ->
+          let (_,_,_,_,osigma) = Proof.proof oldp in
+          Some { it = og; sigma = osigma }
+        | None -> None
+        in
+        let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
+        { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
+      in
+      try
+        Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
+      with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+    end else
+      Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+  with Proof_global.NoCurrentProof -> None;;
 
 let evars () =
   try
@@ -231,10 +255,9 @@ let hints () =
     | [] -> None
     | g :: _ ->
       let env = Goal.V82.env sigma g in
-      let hint_goal = concl_next_tac sigma g in
       let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
       let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
-      Some (hint_hyps, hint_goal)
+      Some (hint_hyps, concl_next_tac)
   with Proof_global.NoCurrentProof -> None
 
 
@@ -273,7 +296,10 @@ let status force =
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
   Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
+  Interface.coq_object_object =
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Pp.string_of_ppcmds (pr_lconstr_env env sigma t.Search.coq_object_object)
 }
 
 let pattern_of_string ?env s =
@@ -283,13 +309,12 @@ let pattern_of_string ?env s =
     | Some e -> e
   in
   let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-  let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in
+  let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in
   pat
 
 let dirpath_of_string_list s =
   let path = String.concat "." s in
-  let m = Pcoq.parse_string Pcoq.Constr.global path in
-  let {CAst.v=qid} = Libnames.qualid_of_reference m in
+  let qid = Pcoq.parse_string Pcoq.Constr.global path in
   let id =
     try Nametab.full_name_module qid
     with Not_found ->
@@ -352,15 +377,12 @@ let about () = {
 }
 
 let handle_exn (e, info) =
-  let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in
   let dummy = Stateid.dummy in
   let loc_of e = match Loc.get_loc e with
     | Some loc -> Some (Loc.unloc loc)
     | _        -> None in
   let mk_msg () = CErrors.print ~info e in
   match e with
-  | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
-  | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -432,7 +454,7 @@ let eval_call c =
   Xmlprotocol.abstract_eval_call handler c
 
 (** Message dispatching.
-    Since coqtop -ideslave starts 1 thread per slave, and each
+    Since [coqidetop] starts 1 thread per slave, and each
     thread forwards feedback messages from the slave to the GUI on the same
     xml channel, we need mutual exclusion.  The mutex should be per-channel, but
     here we only use 1 channel. *)
@@ -460,7 +482,7 @@ let msg_format = ref (fun () ->
 
 (* The loop ignores the command line arguments as the current model delegates
    its handing to the toplevel container. *)
-let loop _args ~state =
+let loop ~opts:_ ~state =
   let open Vernac.State in
   set_doc state.doc;
   init_signal_handler ();
@@ -509,14 +531,16 @@ let rec parse = function
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let () = Coqtop.toploop_init := (fun coq_args extra_args ->
-        let args = parse extra_args in
-        Flags.quiet := true;
-        CoqworkmgrApi.(init 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\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
+
+let islave_init ~opts extra_args =
+  let args = parse extra_args in
+  CoqworkmgrApi.(init High);
+  opts, args
+
+let () =
+  let open Coqtop in
+  let custom = { init = islave_init; run = loop; } in
+  start_coq custom
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index bdb39e94..03396a5a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,6 +37,11 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
+(* Note: Setting the same attribute with two separate tags appears to use
+the first value applied and not the second.  I saw this trying to set the background
+color on Windows.  A clean fix, if ever needed, would be to combine the attributes
+of the tags into a single composite tag before applying.  This is left as an
+exercise for the reader. *)
 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
@@ -50,21 +55,51 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
     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
-    List.iter iter tags
+    List.iter iter (List.rev tags)
+
+let nl_white_regex = Str.regexp "^\\( *\n *\\)"
+let diff_regex = Str.regexp "^diff."
 
 let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
   let open Xml_datatype in
+  let dtags = ref [] in
   let tag name =
     match GtkText.TagTable.lookup buf#tag_table name with
     | None -> raise Not_found
     | Some tag -> new GText.tag tag
   in
   let rmark = `MARK (buf#create_mark buf#start_iter) in
+  (* insert the string, but don't apply diff highlights to white space at the begin/end of line *)
+  let rec insert_str tags s =
+    let etags = try List.hd !dtags :: tags with hd -> tags in
+    try
+      let start = Str.search_forward nl_white_regex s 0 in
+      insert_with_tags buf mark rmark etags (String.sub s 0 start);
+      insert_with_tags buf mark rmark tags (Str.matched_group 1 s);
+      let mend = Str.match_end () in
+      insert_str tags (String.sub s mend (String.length s - mend))
+    with Not_found ->
+      insert_with_tags buf mark rmark etags s
+  in
   let rec insert tags = function
-  | PCData s -> insert_with_tags buf mark rmark tags s
+  | PCData s -> insert_str tags s
   | Element (t, _, children) ->
-    let tags = try tag t :: tags with Not_found -> tags in
-    List.iter (fun xml -> insert tags xml) children
+    let (pfx, tname) = Pp.split_tag t in
+    let is_diff = try let _ = Str.search_forward diff_regex tname 0 in true with Not_found -> false in
+    let (tags, have_tag) =
+      try
+        let t = tag tname in
+        if is_diff && pfx <> Pp.end_pfx then
+          dtags := t :: !dtags;
+        if pfx = "" then
+          ((if is_diff then tags else t :: tags), true)
+        else
+          (tags, true)
+      with Not_found -> (tags, false)
+    in
+    List.iter (fun xml -> insert tags xml) children;
+    if have_tag && is_diff && pfx <> Pp.start_pfx then
+      dtags := (try List.tl !dtags with tl -> []);
   in
   let () = try insert tags msg with _ -> () in
   buf#delete_mark rmark
@@ -289,16 +324,10 @@ let coqtop_path () =
     | Some s -> s
     | None ->
       match cmd_coqtop#get with
-	| Some s -> s
-	| None ->
-	  try
-            let old_prog = Sys.executable_name in
-            let pos = String.length old_prog - 6 in
-            let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos
-            in
-            let new_prog = Bytes.of_string old_prog in
-            Bytes.blit_string "coqtop" 0 new_prog i 6;
-            let new_prog = Bytes.to_string new_prog in
+      | Some s -> s
+      | None ->
+        try
+          let new_prog = System.get_toplevel_path "coqidetop" in
             if Sys.file_exists new_prog then new_prog
 	    else
 	      let in_macos_bundle =
@@ -306,8 +335,8 @@ let coqtop_path () =
 		  (Filename.dirname new_prog)
 		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
 	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
-		 else "coqtop"
-	  with Not_found -> "coqtop"
+                 else "coqidetop"
+        with Not_found -> "coqidetop"
   in file
 
 (* In win32, when a command-line is to be executed via cmd.exe
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index 2be5dce4..f2913b1d 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -153,13 +153,13 @@ let emacs = insert emacs "Emacs" [] [
     i#forward_sentence_end, { s with move = None }));
   mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i ->
     i#backward_sentence_start, { s with move = None }));
-  mkE _n "n" "Move to next line" ~alias:[[],_Down,"DOWN"] (Motion(fun s i ->
+  mkE _n "n" "Move to next line" (Motion(fun s i ->
     let orig_off = Option.default i#line_offset s.move in
     let i = i#forward_line in
     let new_off = min (i#chars_in_line - 1) orig_off in
     (if new_off > 0 then i#set_line_offset new_off else i),
     { s with move = Some orig_off }));
-  mkE _p "p" "Move to previous line" ~alias:[[],_Up,"UP"] (Motion(fun s i ->
+  mkE _p "p" "Move to previous line" (Motion(fun s i ->
     let orig_off = Option.default i#line_offset s.move in
     let i = i#backward_line in
     let new_off = min (i#chars_in_line - 1) orig_off in
@@ -189,7 +189,7 @@ let emacs = insert emacs "Emacs" [] [
       run "Edit" "Cut";
       { s with kill = Some(txt,false); sel = false }
     else s));
-  mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ ->
+  mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ ->
     let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in
     let k =
       if i#ends_line then begin
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 11aaf6e8..955ee878 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -25,6 +25,7 @@ type tag = {
   tag_bold : bool;
   tag_italic : bool;
   tag_underline : bool;
+  tag_strikethrough : bool;
 }
 
 (** Generic preferences *)
@@ -215,15 +216,17 @@ object
     string_of_bool tag.tag_bold;
     string_of_bool tag.tag_italic;
     string_of_bool tag.tag_underline;
+    string_of_bool tag.tag_strikethrough;
   ]
   method into = function
-  | [fg; bg; bd; it; ul] ->
+  | [fg; bg; bd; it; ul; st] ->
     (try Some {
       tag_fg_color = _to fg;
       tag_bg_color = _to bg;
       tag_bold = bool_of_string bd;
       tag_italic = bool_of_string it;
       tag_underline = bool_of_string ul;
+      tag_strikethrough = bool_of_string st;
       }
     with _ -> None)
   | _ -> None
@@ -429,12 +432,13 @@ let tags = ref Util.String.Map.empty
 
 let list_tags () = !tags
 
-let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
+let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) ?(strikethrough = false) () = {
   tag_fg_color = fg;
   tag_bg_color = bg;
   tag_bold = bold;
   tag_italic = italic;
   tag_underline = underline;
+  tag_strikethrough = strikethrough;
 }
 
 let create_tag name default =
@@ -470,6 +474,12 @@ let create_tag name default =
       tag#set_property (`UNDERLINE_SET true);
       tag#set_property (`UNDERLINE `SINGLE)
     end;
+    begin match pref#get.tag_strikethrough with
+    | false -> tag#set_property (`STRIKETHROUGH_SET false)
+    | true ->
+      tag#set_property (`STRIKETHROUGH_SET true);
+      tag#set_property (`STRIKETHROUGH true)
+    end;
   in
   let iter table =
     let tag = GText.tag ~name () in
@@ -480,6 +490,8 @@ let create_tag name default =
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
   tags := Util.String.Map.add name pref !tags
 
+(* note these appear to only set the defaults; they don't override
+the user selection from the Edit/Preferences/Tags dialog *)
 let () =
   let iter (name, tag) = create_tag name tag in
   List.iter iter [
@@ -498,6 +510,10 @@ let () =
     ("tactic.keyword", make_tag ());
     ("tactic.primitive", make_tag ());
     ("tactic.string", make_tag ());
+    ("diff.added", make_tag ~bg:"#b6f1c0" ~underline:true ());
+    ("diff.removed", make_tag ~bg:"#f6b9c1" ~strikethrough:true ());
+    ("diff.added.bg", make_tag ~bg:"#e9feee" ());
+    ("diff.removed.bg", make_tag ~bg:"#fce9eb" ());
   ]
 
 let processed_color =
@@ -549,6 +565,9 @@ let nanoPG =
 let user_queries =
   new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$')
 
+let diffs =
+  new preference ~name:["diffs"] ~init:"off" ~repr:Repr.(string)
+
 class tag_button (box : Gtk.box Gtk.obj) =
 object (self)
 
@@ -561,6 +580,7 @@ object (self)
   val bold = GButton.toggle_button ()
   val italic = GButton.toggle_button ()
   val underline = GButton.toggle_button ()
+  val strikethrough = GButton.toggle_button ()
 
   method set_tag tag =
     let track c but set = match c with
@@ -574,6 +594,7 @@ object (self)
     bold#set_active tag.tag_bold;
     italic#set_active tag.tag_italic;
     underline#set_active tag.tag_underline;
+    strikethrough#set_active tag.tag_strikethrough;
 
   method tag =
     let get but set =
@@ -586,6 +607,7 @@ object (self)
       tag_bold = bold#active;
       tag_italic = italic#active;
       tag_underline = underline#active;
+      tag_strikethrough = strikethrough#active;
     }
 
   initializer
@@ -599,6 +621,7 @@ object (self)
     set_stock bold `BOLD;
     set_stock italic `ITALIC;
     set_stock underline `UNDERLINE;
+    set_stock strikethrough `STRIKETHROUGH;
     box#pack fg_color#coerce;
     box#pack fg_unset#coerce;
     box#pack bg_color#coerce;
@@ -606,6 +629,7 @@ object (self)
     box#pack bold#coerce;
     box#pack italic#coerce;
     box#pack underline#coerce;
+    box#pack strikethrough#coerce;
     let cb but obj = obj#set_sensitive (not but#active) 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
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ccf028ae..dd2976ef 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -21,6 +21,7 @@ type tag = {
   tag_bold : bool;
   tag_italic : bool;
   tag_underline : bool;
+  tag_strikethrough : bool;
 }
 
 class type ['a] repr =
@@ -101,6 +102,7 @@ val tab_length : int preference
 val highlight_current_line : bool preference
 val nanoPG : bool preference
 val user_queries : (string * string) list preference
+val diffs : string preference
 
 val save_pref : unit -> unit
 val load_pref : unit -> unit
diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib
new file mode 100644
index 00000000..8317a086
--- /dev/null
+++ b/ide/protocol/ideprotocol.mllib
@@ -0,0 +1,7 @@
+Xml_lexer
+Xml_parser
+Xml_printer
+Serialize
+Richpp
+Interface
+Xmlprotocol
diff --git a/ide/interface.mli b/ide/protocol/interface.ml
index debbc830..debbc830 100644
--- a/ide/interface.mli
+++ b/ide/protocol/interface.ml
diff --git a/ide/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c..19e9799c 100644
--- a/ide/richpp.ml
+++ b/ide/protocol/richpp.ml
diff --git a/ide/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56..31fc7b56 100644
--- a/ide/richpp.mli
+++ b/ide/protocol/richpp.mli
diff --git a/ide/serialize.ml b/ide/protocol/serialize.ml
index 86074d44..86074d44 100644
--- a/ide/serialize.ml
+++ b/ide/protocol/serialize.ml
diff --git a/ide/serialize.mli b/ide/protocol/serialize.mli
index af082f25..af082f25 100644
--- a/ide/serialize.mli
+++ b/ide/protocol/serialize.mli
diff --git a/ide/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055..e61cb055 100644
--- a/ide/xml_lexer.mli
+++ b/ide/protocol/xml_lexer.mli
diff --git a/ide/xml_lexer.mll b/ide/protocol/xml_lexer.mll
index 4a52147e..4a52147e 100644
--- a/ide/xml_lexer.mll
+++ b/ide/protocol/xml_lexer.mll
diff --git a/ide/xml_parser.ml b/ide/protocol/xml_parser.ml
index 8db3f9e8..8db3f9e8 100644
--- a/ide/xml_parser.ml
+++ b/ide/protocol/xml_parser.ml
diff --git a/ide/xml_parser.mli b/ide/protocol/xml_parser.mli
index ac2eab35..ac2eab35 100644
--- a/ide/xml_parser.mli
+++ b/ide/protocol/xml_parser.mli
diff --git a/ide/xml_printer.ml b/ide/protocol/xml_printer.ml
index 488ef7bf..488ef7bf 100644
--- a/ide/xml_printer.ml
+++ b/ide/protocol/xml_printer.ml
diff --git a/ide/xml_printer.mli b/ide/protocol/xml_printer.mli
index 178f7c80..178f7c80 100644
--- a/ide/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e1821921..e1821921 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
diff --git a/ide/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0..ba6000f0 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 8eddfb31..06281d62 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -98,7 +98,7 @@ object(self)
 	~packing:(vbox#pack ~fill:true ~expand:true) () in
     let result = Wg_MessageView.message_view () in
     router#register_route route_id result;
-    r_bin#add (result :> GObj.widget);
+    r_bin#add_with_viewport (result :> GObj.widget);
     views <- (frame#coerce, result, combo#entry) :: views;
     let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
@@ -152,9 +152,9 @@ object(self)
   method show =
     frame#show;
     let cur_page = notebook#get_nth_page notebook#current_page in
-    let _, _, e =
-      List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in
-    e#misc#grab_focus ()
+    match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with
+    | (_, _, e) -> e#misc#grab_focus ()
+    | exception Not_found -> ()
 
   method hide =
     frame#hide