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