From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 toplevel/coqtop.ml | 30 ++++++++++++++++++------------
 1 file changed, 18 insertions(+), 12 deletions(-)

(limited to 'toplevel/coqtop.ml')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c3f79e0a..6d65ccc2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml 7740 2005-12-26 20:07:21Z herbelin $ *)
+(* $Id: coqtop.ml 8932 2006-06-09 09:29:03Z notin $ *)
 
 open Pp
 open Util
@@ -108,14 +108,16 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
-  List.iter
-    (fun (v,f) ->
-      States.unfreeze init_state;
-      if Options.do_translate () then
-	with_option translate_file (Vernac.compile v) f
-      else
-	Vernac.compile v f)
-    (List.rev !compile_list)
+  let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+    List.iter
+      (fun (v,f) ->
+	 States.unfreeze init_state;
+	 Constrintern.coqdoc_unfreeze coqdoc_init_state;
+	 if Options.do_translate () then
+	   with_option translate_file (Vernac.compile v) f
+	 else
+	   Vernac.compile v f)
+      (List.rev !compile_list)
 
 let re_exec_version = ref ""
 let set_byte () = re_exec_version := "byte"
@@ -172,7 +174,11 @@ let ide_args = ref []
 let parse_args is_ide =
   let rec parse = function
     | [] -> ()
-
+    | "-with-geoproof" :: s :: rem -> 
+	if s = "yes" then Coq_config.with_geoproof := true
+	else if s = "no" then Coq_config.with_geoproof := false
+	else usage ();
+	parse rem
     | "-impredicative-set" :: rem -> 
         set_engagement Declarations.ImpredicativeSet; parse rem
 
@@ -242,9 +248,9 @@ let parse_args is_ide =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-vm" :: rem -> use_vm := true; parse rem
-    | "-emacs" :: rem -> Options.print_emacs := true; parse rem
+    | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem
 	  
-    | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
+    | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
 
     | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem
 
-- 
cgit v1.2.3