From aa60931752217a7bf0536acae4e7858f48eb8c8e Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Mon, 30 Jan 2017 21:08:29 +0100
Subject: fix Emacs compiler warning on '(lambda...)

lambda is self-quoting, see elisp manual, section 12.7 Anonymous
Functions
---
 tools/gallina-db.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/gallina-db.el b/tools/gallina-db.el
index baabebb13a..9664f69f8b 100644
--- a/tools/gallina-db.el
+++ b/tools/gallina-db.el
@@ -163,7 +163,7 @@ for DB structure."
 
 (defun coq-sort-menu-entries (menu)
   (sort menu 
-	'(lambda (x y) (string< 
+	(lambda (x y) (string< 
 			(downcase (elt x 0)) 
 			(downcase (elt y 0))))))
 
-- 
cgit v1.2.3


From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 18 Dec 2016 18:14:58 +0100
Subject: [stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
---
 tools/coq_makefile.ml | 2 +-
 tools/coqmktop.ml     | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7dd5f2a14..624b9ced7d 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -51,7 +51,7 @@ let lib_dirs =
   ["kernel"; "lib"; "library"; "parsing";
    "pretyping"; "interp"; "printing"; "intf";
    "proofs"; "tactics"; "tools"; "ltacprof";
-   "toplevel"; "stm"; "grammar"; "config";
+   "vernac"; "stm"; "toplevel"; "grammar"; "config";
    "ltac"; "engine"]
 
 
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index eaf938e8ce..645b3665e0 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -75,6 +75,7 @@ let std_includes basedir =
   let rebase d = match basedir with None -> d | Some base -> base / d in
   ["-I"; rebase ".";
    "-I"; rebase "lib";
+   "-I"; rebase "vernac";       (* For Mltop *)
    "-I"; rebase "toplevel";
    "-I"; rebase "kernel/byterun";
    "-I"; Envars.camlp4lib () ] @
-- 
cgit v1.2.3


From b09751b9a1b48541acc9a2daaff9ebc453fc3bf7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Feb 2017 19:05:45 +0100
Subject: Removing spurious folder includes in coq_makefile.

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

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 624b9ced7d..4842a89151 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -50,9 +50,9 @@ let section s =
 let lib_dirs =
   ["kernel"; "lib"; "library"; "parsing";
    "pretyping"; "interp"; "printing"; "intf";
-   "proofs"; "tactics"; "tools"; "ltacprof";
+   "proofs"; "tactics"; "tools";
    "vernac"; "stm"; "toplevel"; "grammar"; "config";
-   "ltac"; "engine"]
+   "engine"]
 
 
 let usage () =
-- 
cgit v1.2.3


From 53d30eb8b3186031658dafd74dc7ad012854f385 Mon Sep 17 00:00:00 2001
From: Vadim Zaliva
Date: Wed, 8 Mar 2017 23:05:55 -0800
Subject: Fix #5132: coq_makefile generates incorrect install goal

---
 tools/coq_makefile.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b7dd5f2a14..294575e0a5 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -676,6 +676,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "VO=vo\n";
       print "VOFILES:=$(VFILES:.v=.$(VO))\n";
       classify_files_by_root "VOFILES" l inc;
+      classify_files_by_root "VFILES" l inc;
       print "GLOBFILES:=$(VFILES:.v=.glob)\n";
       print "GFILES:=$(VFILES:.v=.g)\n";
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
-- 
cgit v1.2.3


From 92579449f62f0fd7699b0b447f3aee0d82d1b5c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 13:48:47 +0100
Subject: [safe-string] tools

No functional changes.
---
 tools/coq_makefile.ml | 7 ++-----
 tools/coqdoc/alpha.ml | 7 +------
 tools/coqdoc/index.ml | 4 ++--
 tools/coqworkmgr.ml   | 9 ++++++---
 4 files changed, 11 insertions(+), 16 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4842a89151..23479aee52 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -125,12 +125,9 @@ let physical_dir_of_logical_dir ldir =
   let le = String.length ldir - 1 in
   let pdir =
     if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1)
-    else String.copy ldir
+    else ldir
   in
-  for i = 0 to le - 1 do
-    if pdir.[i] = '.' then pdir.[i] <- '/';
-  done;
-  pdir
+  String.map (fun c -> if c = '.' then '/' else c) pdir
 
 let standard opt =
   print "byte:\n";
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a2a..3d92c9356b 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -26,12 +26,7 @@ let norm_char c =
   if !latin1 then norm_char_latin1 c else
   Char.uppercase c
 
-let norm_string s =
-  let u = String.copy s in
-  for i = 0 to String.length s - 1 do
-    u.[i] <- norm_char s.[i]
-  done;
-  u
+let norm_string = String.map (fun s -> norm_char s)
 
 let compare_char c1 c2 = match norm_char c1, norm_char c2 with
   | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8de..c9cb676e98 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -197,7 +197,7 @@ let prepare_entry s = function
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
       let sc = String.sub s (h+1) (i-h-1) in
-      let ntn = String.make (String.length s - i) ' ' in
+      let ntn = Bytes.make (String.length s - i) ' ' in
       let k = ref 0 in
       let j = ref (i+1) in
       let quoted = ref false in
@@ -220,7 +220,7 @@ let prepare_entry s = function
 	  end;
 	incr j
       done;
-      let ntn = String.sub ntn 0 !k in
+      let ntn = Bytes.sub_string ntn 0 !k in
       if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
   | _ ->
       s
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index d7bdf907a2..b8e69d6c6d 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -72,10 +72,13 @@ let really_read_fd fd s off len =
 let raw_input_line fd =
   try
     let b = Buffer.create 80 in
-    let s = String.make 1 '\000' in
-    while s <> "\n" do
+    let s = Bytes.make 1 '\000' in
+    let endl = Bytes.of_string "\n" in
+    let endr = Bytes.of_string "\r" in
+    while Bytes.compare s endl <> 0 do
       really_read_fd fd s 0 1;
-      if s <> "\n" && s <> "\r" then Buffer.add_string b s;
+      if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0
+      then Buffer.add_bytes b s;
     done;
     Buffer.contents b
   with Unix.Unix_error _ -> raise End_of_file
-- 
cgit v1.2.3


From 5e2574cbef1ba132aacc73b4a079cc0b5584f589 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 14:57:59 +0100
Subject: [safe-string] Enable -safe-string !

We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.

- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
---
 tools/coq_makefile.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 23479aee52..4dfb7af6aa 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -521,10 +521,10 @@ let variables is_install opt (args,defs) =
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
-    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
-    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
-    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n";
+    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n";
+    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n";
+    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n";
     print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
     print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
     print "GRAMMARS?=grammar.cma\n";
@@ -764,9 +764,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
       print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
       print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
     end;
   if !some_vfile then
     begin
@@ -882,7 +882,7 @@ let check_overlapping_include (_,inc_i,inc_r) =
  *)
 let merlin targets (ml_inc,_,_) =
   print ".merlin:\n";
-  print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+  print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ;
   List.iter (fun c ->
       printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
     lib_dirs ;
-- 
cgit v1.2.3


From d25b1431eb73a04bdfc0f1ad2922819b69bba93a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Mar 2017 15:14:01 +0100
Subject: [misc] Remove warnings about String.set

The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
---
 tools/coqdoc/index.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index c9cb676e98..34108eff42 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -205,17 +205,17 @@ let prepare_entry s = function
       while !j <= l do
 	if not !quoted then begin
 	  (match s.[!j] with
-	  | '_' -> ntn.[!k] <- ' '; incr k
-	  | 'x' -> ntn.[!k] <- '_'; incr k
+	  | '_' -> Bytes.set ntn !k ' '; incr k
+	  | 'x' -> Bytes.set ntn !k '_'; incr k
 	  | '\'' -> quoted := true
 	  | _ -> assert false)
 	end
 	else
 	  if s.[!j] = '\'' then
 	    if (!j = l || s.[!j+1] = '_') then quoted := false
-	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
+	    else (incr j; Bytes.set ntn !k s.[!j]; incr k)
 	  else begin
-	    ntn.[!k] <- s.[!j];
+	    Bytes.set ntn !k s.[!j];
 	    incr k
 	  end;
 	incr j
-- 
cgit v1.2.3


From f1c5e2ce2a4515a7c90c5ca22aa6eff22dd2f5ff Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 28 Jun 2016 16:52:46 +0200
Subject: [ide] Use "log via feedback".

We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
---
 tools/fake_ide.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535d1..23c111b371 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -37,14 +37,9 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    match Xmlprotocol.is_message xml with
-    | Some (level, _loc, content) ->
-      logger level content;
+    if Xmlprotocol.is_feedback xml then
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then
-        loop ()
-      else Xmlprotocol.to_answer call xml
+    else Xmlprotocol.to_answer call xml
   in
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);
-- 
cgit v1.2.3


From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 29 Sep 2016 16:30:21 +0200
Subject: [pp] Make feedback the only logging mechanism.

Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.

This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.

Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.

However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.

The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.

We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.

`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.

Thus, the new panorama is:

- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
  It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
  to coqtop.

_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.

_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.

A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.

The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
---
 tools/fake_ide.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 23c111b371..e89f19041f 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -29,7 +29,7 @@ let error_xml s =
   exit 1
 
 let logger level content =
-  Printf.eprintf "%a\n%! " print_xml (Richpp.repr content)
+  Printf.eprintf "%a\n%! " print_xml Richpp.(content |> richpp_of_pp |> repr)
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -44,8 +44,8 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);
   match res with
-  | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s)
-  | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x
+  | Interface.Fail (_,_,s) when fail -> error_xml Richpp.(s |> richpp_of_pp |> repr)
+  | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml Richpp.(s |> richpp_of_pp |> repr); x
   | x -> x
 
 let eval_call c q = ignore(base_eval_call c q)
@@ -194,7 +194,7 @@ let print_document () =
 module GUILogic = struct
 
   let after_add = function
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+    | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s))
     | Interface.Good (id, (Util.Inl (), _)) ->
         Document.assign_tip_id doc id
     | Interface.Good (id, (Util.Inr tip, _)) ->
@@ -206,7 +206,7 @@ module GUILogic = struct
   let at id id' _ = Stateid.equal id' id
   
   let after_edit_at (id,need_unfocus) = function
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+    | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s))
     | Interface.Good (Util.Inl ()) ->
         if need_unfocus then Document.unfocus doc;
         ignore(Document.cut_at doc id);
@@ -329,7 +329,7 @@ let main =
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
     | Interface.Good _ -> exit 0
-    | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
+    | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s)) in
   (* The main loop *)
   init ();
   while true do
-- 
cgit v1.2.3


From a010de9bcaa33fc95a2a7cb6478ac21c95e3ad9e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 30 Nov 2016 22:18:30 +0100
Subject: [pp] Remove richpp from fake_ide.

---
 tools/fake_ide.ml | 25 +++++++------------------
 1 file changed, 7 insertions(+), 18 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index e89f19041f..b538ba1d04 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -17,19 +17,8 @@ type coqtop = {
   xml_parser : Xml_parser.t;
 }
 
-let print_xml chan xml =
-  let rec print = function
-  | Xml_datatype.PCData s -> output_string chan s
-  | Xml_datatype.Element (_, _, children) -> List.iter print children
-  in
-  print xml
-
-let error_xml s =
-  Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
-  exit 1
-
-let logger level content =
-  Printf.eprintf "%a\n%! " print_xml Richpp.(content |> richpp_of_pp |> repr)
+let print_error msg =
+  Format.eprintf "fake_id: error: @[%a@]\n%!" (Pp.pp_with ?pp_tag:None) msg
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -44,8 +33,8 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);
   match res with
-  | Interface.Fail (_,_,s) when fail -> error_xml Richpp.(s |> richpp_of_pp |> repr)
-  | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml Richpp.(s |> richpp_of_pp |> repr); x
+  | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
+  | Interface.Fail (_,_,s) as x      -> print_error s; x
   | x -> x
 
 let eval_call c q = ignore(base_eval_call c q)
@@ -194,7 +183,7 @@ let print_document () =
 module GUILogic = struct
 
   let after_add = function
-    | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s))
+    | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (id, (Util.Inl (), _)) ->
         Document.assign_tip_id doc id
     | Interface.Good (id, (Util.Inr tip, _)) ->
@@ -206,7 +195,7 @@ module GUILogic = struct
   let at id id' _ = Stateid.equal id' id
   
   let after_edit_at (id,need_unfocus) = function
-    | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s))
+    | Interface.Fail (_,_,s) -> print_error s; exit 1
     | Interface.Good (Util.Inl ()) ->
         if need_unfocus then Document.unfocus doc;
         ignore(Document.cut_at doc id);
@@ -329,7 +318,7 @@ let main =
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
     | Interface.Good _ -> exit 0
-    | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s)) in
+    | Interface.Fail (_,_,s) -> print_error s; exit 1 in
   (* The main loop *)
   init ();
   while true do
-- 
cgit v1.2.3


From a8ec2dc5c330ded1ba400ef202c57e68d2533312 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 5 Dec 2016 18:17:46 +0100
Subject: [pp] Remove special tag type and handler from Pp.

For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.

We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.

This is a step towards moving the last bit of terminal code out of the
core system.
---
 tools/fake_ide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index b538ba1d04..5dd2a92200 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -18,7 +18,7 @@ type coqtop = {
 }
 
 let print_error msg =
-  Format.eprintf "fake_id: error: @[%a@]\n%!" (Pp.pp_with ?pp_tag:None) msg
+  Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
 
 let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   if print then prerr_endline (Xmlprotocol.pr_call call);
-- 
cgit v1.2.3


From 921ea3983d45051ae85b0e20bf13de2eff38e53e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 8 Feb 2017 18:13:25 +0100
Subject: [pp] Remove uses of expensive string_of_ppcmds.

In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
---
 tools/fake_ide.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 5dd2a92200..7a891239bd 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,6 +12,8 @@ let error s =
   prerr_endline ("fake_id: error: "^s);
   exit 1
 
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
 type coqtop = {
   xml_printer : Xml_printer.t;
   xml_parser : Xml_parser.t;
@@ -170,7 +172,7 @@ let print_document () =
           Str.global_replace (Str.regexp "^[\n ]*") ""
       (if String.length s > 20 then String.sub s 0 17 ^ "..."
        else s) in
-  prerr_endline (Pp.string_of_ppcmds
+  pperr_endline (
     (Document.print doc
       (fun b state_id { name; text } ->
         Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
-- 
cgit v1.2.3


From 829a8feb3d02da057d39b5029b422e8a45dd1608 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 25 Jan 2017 14:39:29 +0100
Subject: [xml] Restore protocol compatibility with 8.6.

By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`
---
 tools/fake_ide.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 7a891239bd..932097607b 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -296,11 +296,12 @@ let main =
   Sys.set_signal Sys.sigpipe
     (Sys.Signal_handle
        (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
+  let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
   let coqtop_name, coqtop_args, input_file = match Sys.argv with
-    | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+    | [| _; f |] -> "coqtop", Array.of_list def_args, f
     | [| _; f; ct |] ->
         let ct = Str.split (Str.regexp " ") ct in
-        List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+        List.hd ct, Array.of_list (def_args @ List.tl ct), f
     | _ -> usage () in
   let inc = if input_file = "-" then stdin else open_in input_file in
   let coq =
-- 
cgit v1.2.3