summaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /toplevel/coqtop.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml65
1 files changed, 38 insertions, 27 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3374b0ee..e6d2deec 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml 9191 2006-09-29 15:45:42Z courtieu $ *)
+(* $Id: coqtop.ml 11062 2008-06-06 14:19:50Z notin $ *)
open Pp
open Util
open System
-open Options
+open Flags
open Names
open Libnames
open Nameops
@@ -32,6 +32,8 @@ let print_header () =
Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
flush stdout
+let output_context = ref false
+
let memory_stat = ref false
let print_memory_stat () =
@@ -81,7 +83,7 @@ let add_load_vernacular verb s =
let load_vernacular () =
List.iter
(fun (s,b) ->
- if Options.do_translate () then
+ if Flags.do_translate () then
with_option translate_file (Vernac.load_vernac b) s
else
Vernac.load_vernac b s)
@@ -102,7 +104,7 @@ let require () =
let compile_list = ref ([] : (bool * string) list)
let add_compile verbose s =
set_batch_mode ();
- Options.make_silent true;
+ Flags.make_silent true;
compile_list := (verbose,s) :: !compile_list
let compile_files () =
let init_state = States.freeze() in
@@ -111,7 +113,7 @@ let compile_files () =
(fun (v,f) ->
States.unfreeze init_state;
Constrintern.coqdoc_unfreeze coqdoc_init_state;
- if Options.do_translate () then
+ if Flags.do_translate () then
with_option translate_file (Vernac.compile v) f
else
Vernac.compile v f)
@@ -129,6 +131,11 @@ let set_opt () = re_exec_version := "opt"
let re_exec is_ide =
let s = !re_exec_version in
let is_native = (Mltop.get()) = Mltop.Native in
+ (* Unix.readlink is not implemented on Windows architectures :-(
+ let prog =
+ try Unix.readlink "/proc/self/exe"
+ with Unix.Unix_error _ -> Sys.argv.(0) in
+ *)
let prog = Sys.argv.(0) in
if (is_native && s = "byte") || ((not is_native) && s = "opt")
then begin
@@ -151,7 +158,7 @@ let use_vm = ref false
let set_vm_opt () =
Vm.set_transp_values (not !boxed_val);
- Options.set_boxed_definitions !boxed_def;
+ Flags.set_boxed_definitions !boxed_def;
Vconv.set_use_vm !use_vm
(*s Parsing of the command line.
@@ -236,7 +243,7 @@ let parse_args is_ide =
| "-compile-verbose" :: f :: rem -> add_compile true f; parse rem
| "-compile-verbose" :: [] -> usage ()
- | "-dont-load-proofs" :: rem -> Options.dont_load_proofs := true; parse rem
+ | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem
| "-translate" :: rem -> make_translate true; parse rem
@@ -246,13 +253,15 @@ let parse_args is_ide =
| "-debug" :: rem -> set_debug (); parse rem
| "-vm" :: rem -> use_vm := true; parse rem
- | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem
- | "-emacs-U" :: rem -> Options.print_emacs := true;
- Options.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
-
+ | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+ | "-emacs-U" :: rem -> Flags.print_emacs := true;
+ Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
+
+ | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
+
| "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
- | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem
+ | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
@@ -270,13 +279,15 @@ let parse_args is_ide =
| ("-m" | "--memory") :: rem -> memory_stat := true; parse rem
- | "-xml" :: rem -> Options.xml_export := true; parse rem
+ | "-xml" :: rem -> Flags.xml_export := true; parse rem
+
+ | "-output-context" :: rem -> output_context := true; parse rem
- (* Scanned in Options! *)
+ (* Scanned in Flags. *)
| "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
| "-v8" :: rem -> parse rem
- | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem
+ | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
| s :: rem ->
if is_ide then begin
@@ -297,15 +308,10 @@ let parse_args is_ide =
end
| e -> begin msgnl (Cerrors.explain_exn e); exit 1 end
-
-(* To prevent from doing the initialization twice *)
-let initialized = ref false
-
let init is_ide =
- if not !initialized then begin
- initialized := true;
- Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
- Lib.init();
+ Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+ Lib.init();
+ begin
try
parse_args is_ide;
re_exec is_ide;
@@ -315,21 +321,26 @@ let init is_ide =
set_vm_opt ();
engage ();
if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
- option_iter Declaremods.start_library !toplevel_name;
+ Option.iter Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();
load_rcfile();
load_vernacular ();
compile_files ();
- outputstate ();
+ outputstate ()
with e ->
flush_all();
- if not !batch_mode then message "Error during initialization :";
+ if not !batch_mode then message "Error during initialization:";
msgnl (Toplevel.print_toplevel_error e);
exit 1
end;
- if !batch_mode then (flush_all(); Profile.print_profile (); exit 0);
+ if !batch_mode then
+ (flush_all();
+ if !output_context then
+ Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
+ Profile.print_profile ();
+ exit 0);
Lib.declare_initial_state ()
let init_ide () = init true; List.rev !ide_args