From 41f0f4a53fd462cd7e0bb190ebd547409a0873de Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 18 May 2015 14:50:28 +0200
Subject: Adding the -color option to coqc.

coqc by default uses colors, this allows to disable it. Moreover,
colors are not yet correctly disabled when compiling from emacs (emacs
bugs?), making this option even more useful.
---
 tools/coqc.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index aed229abc8..5710b97f2a 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -111,18 +111,18 @@ let parse_args () =
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-verbose-compat-notations"|"-no-compat-notations"
-      |"-indices-matter"|"-quick"|"-color"|"-type-in-type"
+      |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       as o) :: rem ->
 	parse (cfiles,o::args) rem
 
 (* Options for coqtop : b) options with 1 argument *)
 
-    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
+    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
-      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w"
+      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
       as o) :: rem ->
 	begin
 	  match rem with
-- 
cgit v1.2.3


From c6714db203f60413523ebeaac86242a6e4cc05e3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 27 May 2015 11:43:10 +0200
Subject: Test for 4159

---
 tools/fake_ide.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tools')

diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index c2b126687f..d7a292f4cf 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -257,6 +257,9 @@ let eval_print l coq =
   | [ Tok(_,"WAIT") ] ->
       let phrase = "Stm Wait." in
       eval_call (query (phrase,tip_id())) coq
+  | [ Tok(_,"JOIN") ] ->
+      let phrase = "Stm JoinDocument." in
+      eval_call (query (phrase,tip_id())) coq
   | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
       let to_id, _ = get_id id in
       if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
@@ -273,6 +276,7 @@ let grammar =
     ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
     ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
     ; Seq [Item (eat_rex "WAIT")]
+    ; Seq [Item (eat_rex "JOIN")]
     ; Seq [Item (eat_rex "GOALS")]
     ; Seq [Item (eat_rex "FAILGOALS")]
     ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
-- 
cgit v1.2.3