From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

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

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bf86db08ff..ca0ef38d32 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -82,7 +82,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.
    *
-- 
cgit v1.2.3


From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 22 Apr 2017 12:55:46 +0200
Subject: Warning 29: non escaped end of line may be non portable

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

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ca0ef38d32..dbfe4256b3 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -512,5 +512,5 @@ let () = Coqtop.toploop_init := (fun 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"
-- 
cgit v1.2.3


From 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:03:54 +0200
Subject: Remove uses of [Flags.make_silent]

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

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dbfe4256b3..966a94da91 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -505,7 +505,7 @@ 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)
 
-- 
cgit v1.2.3


From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 26 Apr 2017 11:57:58 +0200
Subject: Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.
---
 ide/ide_slave.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 966a94da91..56ada9d132 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)
-- 
cgit v1.2.3


From 6a412da0f2681ede8f2753666bb9098e7ac8bfd2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 May 2017 02:55:28 +0200
Subject: [ide] Disable `print_ast` call.

So far this part of the system has shown little utility other than
having developers put time to fix it every time they change something
in the system.

I have never seen this functionality used in the wild, and a large
part of the vernac was marked TODO. Given that we have automatic
methods to provide this functionality these days (PPX), we remove
Texmacspp.
---
 ide/ide_slave.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'ide/ide_slave.ml')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 56ada9d132..dbca959eae 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -388,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 (expr, loc) -> begin
-      try  Texmacspp.tmpp expr loc
-      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 *)
 
-- 
cgit v1.2.3