From 5da573031d36c5a1df5dcf64cc8764f489f774f7 Mon Sep 17 00:00:00 2001
From: CJ Bell
Date: Thu, 10 Nov 2016 22:28:13 -0500
Subject: Remove unused feedback_content: Goals

---
 ide/xmlprotocol.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ide')

diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index aecb317bcb..5f82a8898b 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -816,7 +816,6 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "workerstatus", [ns] ->
        let n, s = to_pair to_string to_string ns in
        WorkerStatus(n,s)
-  | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
   | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
   | "filedependency", [from; dep] ->
       FileDependency (to_option to_string from, to_string dep)
@@ -849,8 +848,6 @@ let of_feedback_content = function
   | WorkerStatus(n,s) ->
       constructor "feedback_content" "workerstatus"
         [of_pair of_string of_string (n,s)]
-  | Goals (loc,s) ->
-      constructor "feedback_content" "goals" [of_loc loc;of_string s]
   | Custom (loc, name, x) ->
       constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
   | FileDependency (from, depends_on) ->
-- 
cgit v1.2.3


From dd47fcfc08c43288a49797cc72829da3f9642094 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Nov 2016 10:57:47 +0100
Subject: Making explicit that a result is discarded (ocaml warning).

---
 ide/preferences.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 64327d74f5..b16d45b549 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -468,7 +468,7 @@ let create_tag name default =
   let iter table =
     let tag = GText.tag ~name () in
     table#add tag#as_tag;
-    pref#connect#changed (fun _ -> set_tag tag);
+    ignore (pref#connect#changed (fun _ -> set_tag tag));
     set_tag tag;
   in
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
-- 
cgit v1.2.3


From 7e992fa784ee6fa48af8a2e461385c094985587d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Nov 2016 11:20:38 +0100
Subject: Coqide: fixing default local links for refman and stdlib.

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

(limited to 'ide')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index b16d45b549..f0fd45d77f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -918,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () =
   in
   let doc_url =
     let predefined = [
-      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]);
+      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]);
       Coq_config.wwwrefman;
       use_default_doc_url
     ] in
@@ -931,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () =
       doc_url#get in
   let library_url =
     let predefined = [
-      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]);
+      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]);
       Coq_config.wwwstdlib
     ] in
     combo
-- 
cgit v1.2.3


From 26d180fa0b27edc773fd07c73906e4ed56475200 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 16 Nov 2016 10:51:39 +0100
Subject: [stm] Remove STM-related vernaculars

I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.

The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
---
 ide/texmacspp.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 680da7f54b..dbcd8630b1 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,9 +724,6 @@ let rec tmpp v loc =
   | VernacComments (cl) ->
       xmlComment loc (List.flatten (List.map pp_comment cl))
 
-  (* Stm backdoor *)
-  | VernacStm _ as x -> xmlTODO loc x
-
   (* Proof management *)
   | VernacGoal _ as x -> xmlTODO loc x
   | VernacAbort _ as x -> xmlTODO loc x
-- 
cgit v1.2.3


From bdcf5b040b975a179fe9b2889fea0d38ae4689df Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Nov 2016 08:38:30 +0100
Subject: Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"

This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing
changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341.

It turns out that calling from fake_ide the STM commands that were removed
by this PR requires an extension of the XML protocol. So postponing the
integration.
---
 ide/texmacspp.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index dbcd8630b1..680da7f54b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,6 +724,9 @@ let rec tmpp v loc =
   | VernacComments (cl) ->
       xmlComment loc (List.flatten (List.map pp_comment cl))
 
+  (* Stm backdoor *)
+  | VernacStm _ as x -> xmlTODO loc x
+
   (* Proof management *)
   | VernacGoal _ as x -> xmlTODO loc x
   | VernacAbort _ as x -> xmlTODO loc x
-- 
cgit v1.2.3


From 9ddae1778aef70c55a1347c4d0b28694cf34a5af Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 13:39:06 +0100
Subject: Fix some documentation typos.

---
 ide/utils/configwin_keys.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index 9f44e5c6be..e9b19da621 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -154,7 +154,7 @@ let xk_KP_9			= 0xFFB9
 
 
 (*
- * Auxilliary Functions; note the duplicate definitions for left and right
+ * Auxiliary Functions; note the duplicate definitions for left and right
  * function keys;  Sun keyboards and a few other manufactures have such
  * function key groups on the left and/or right sides of the keyboard.
  * We've not found a keyboard with more than 35 function keys total.
-- 
cgit v1.2.3


From f35eb5737fcdc1430eb45372d5bb99109d0216a2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 28 Jun 2016 16:51:59 +0200
Subject: [merlin] Adjust merlin for ide.

---
 ide/.merlin | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/.merlin b/ide/.merlin
index 3f3d9d275d..953b5dce4c 100644
--- a/ide/.merlin
+++ b/ide/.merlin
@@ -1,4 +1,4 @@
-PKG lablgtk2.sourceview2
+PKG unix laglgtk2 lablgtk2.sourceview2
 
 S utils
 B utils
-- 
cgit v1.2.3


From aa21c209f85f37b3d16ff499bbeac15e967bf78f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 13 Jan 2017 08:40:17 +0100
Subject: Fix broken .aux machinery.

Coq expects aux_file_name_for to give the aux file corresponding to the
input file whichever its Coq-related extension, be it .v or .vo or .vio.
Commit 3e6fa1c broke this contract when fixing bug #5183. As a
consequence, depending on the execution path, Coq would try to save or
load from either .foo.aux or .foo.vo.aux or .foo.vio.aux.

This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call
chain by not initializing hints when the input file does not end with .v.
This also restores 8.5 behavior with respect to aux file naming.
---
 ide/ide_slave.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 5b07d3ec3b..c0c4131ac5 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -392,7 +392,8 @@ let init =
              Stm.add false ~ontop:(Stm.get_current_state ())
                0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
            else Stm.get_current_state (), `NewTip in
-         Stm.set_compilation_hints file;
+         if Filename.check_suffix file ".v" then
+           Stm.set_compilation_hints file;
          Stm.finish ();
          initial_id
    end
-- 
cgit v1.2.3


From 22e2e5722d233bbd939cd235650497e30e506e63 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 27 Jan 2017 09:29:53 +0100
Subject: Fix documentation typos.

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

(limited to 'ide')

diff --git a/ide/interface.mli b/ide/interface.mli
index 2a9b8b241f..123cac6c22 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -139,7 +139,7 @@ type add_rty = state_id * ((unit, state_id) union * string)
     [Inr (start,(stop,tip))] if [id] is in a zone that can be focused.
     In that case the zone is delimited by [start] and [stop] while [tip]
     is the new document [tip].  Edits made by subsequent [add] are always
-    performend on top of [id]. *)
+    performed on top of [id]. *)
 type edit_at_sty = state_id
 type edit_at_rty = (unit, state_id * (state_id * state_id)) union
 
@@ -153,7 +153,7 @@ type query_rty = string
 type goals_sty = unit
 type goals_rty = goals option
 
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+(** Retrieve the list of uninstantiated evars in the current proof. [None] if no
     proof is in progress. *)
 type evars_sty = unit
 type evars_rty = evar list option
-- 
cgit v1.2.3