diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 114 |
1 files changed, 46 insertions, 68 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7887a060..76e9c2fe 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open System @@ -122,51 +120,19 @@ let compile_files () = (List.rev !compile_list) let set_compat_version = function + | "8.3" -> compat_version := Some V8_3 | "8.2" -> compat_version := Some V8_2 | "8.1" -> warning "Compatibility with version 8.1 not supported." | "8.0" -> warning "Compatibility with version 8.0 not supported." | s -> error ("Unknown compatibility version \""^s^"\".") -let re_exec_version = ref "" -let set_byte () = re_exec_version := "byte" -let set_opt () = re_exec_version := "opt" - -(* Re-exec Coq in bytecode or native code if necessary. [s] is either - ["byte"] or ["opt"]. Notice that this is possible since the nature of - the toplevel has already been set in [Mltop] by the main file created - by coqmktop (see scripts/coqmktop.ml). *) - -let re_exec is_ide = - let s = !re_exec_version in - let is_native = Mltop.is_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 - let s = if s = "" then if is_native then "opt" else "byte" else s in - let newprog = - let dir = Filename.dirname prog in - let coqtop = if is_ide then "coqide." else "coqtop." in - let com = coqtop ^ s ^ Coq_config.exec_extension in - if dir <> "." then Filename.concat dir com else com - in - Sys.argv.(0) <- newprog; - Unix.handle_unix_error (Unix.execvp newprog) Sys.argv - end - (*s options for the virtual machine *) let boxed_val = ref false -let boxed_def = ref false let use_vm = ref false let set_vm_opt () = Vm.set_transp_values (not !boxed_val); - Flags.set_boxed_definitions !boxed_def; Vconv.set_use_vm !use_vm (*s Parsing of the command line. @@ -183,12 +149,13 @@ let usage () = let warning s = msg_warning (str s) +let ide_slave = ref false +let filter_opts = ref false -let ide_args = ref [] -let parse_args is_ide = +let parse_args arglist = let glob_opt = ref false in 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 @@ -216,14 +183,15 @@ let parse_args is_ide = | "-notop" :: rem -> unset_toplevel_name (); parse rem | "-q" :: rem -> no_load_rc (); parse rem - | "-opt" :: rem -> set_opt(); parse rem - | "-byte" :: rem -> set_byte(); parse rem + | "-opt" :: rem -> warning "option -opt deprecated, call with .opt suffix\n"; parse rem + | "-byte" :: rem -> warning "option -byte deprecated, call with .byte suffix\n"; parse rem | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem | "-boot" :: rem -> boot := true; no_load_rc (); parse rem | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem - | "-outputstate" :: s :: rem -> set_outputstate s; parse rem + | "-outputstate" :: s :: rem -> + Flags.load_proofs := Flags.Force; set_outputstate s; parse rem | "-outputstate" :: [] -> usage () | "-nois" :: rem -> set_inputstate ""; parse rem @@ -264,7 +232,9 @@ let parse_args is_ide = | "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem | "-compile-verbose" :: [] -> usage () - | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem + | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem + | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem + | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem | "-beautify" :: rem -> make_beautify true; parse rem @@ -278,30 +248,28 @@ let parse_args is_ide = | "-vm" :: rem -> use_vm := true; 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 + | "-emacs-U" :: rem -> + warning "Obsolete option \"-emacs-U\", use -emacs instead."; + Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-unicode" :: rem -> add_require "Utf8_core"; parse rem | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem | "-coqlib" :: [] -> usage () - | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0 + | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0) - | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 + | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0) | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-v"|"--version") :: _ -> Usage.version () + | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0) | "-init-file" :: f :: rem -> set_rcfile f; parse rem | "-init-file" :: [] -> usage () - | "-user" :: u :: rem -> set_rcuser u; parse rem - | "-user" :: [] -> usage () - | "-notactics" :: rem -> warning "Obsolete option \"-notactics\"."; remove_top_ml (); parse rem @@ -320,32 +288,41 @@ let parse_args is_ide = | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem + | "-ideslave" :: rem -> ide_slave := true; parse rem + + | "-filteropts" :: rem -> filter_opts := true; parse rem + | s :: rem -> - if is_ide then begin - ide_args := s :: !ide_args; - parse rem - end else begin - prerr_endline ("Don't know what to do with " ^ s); usage () - end + if !filter_opts then + s :: (parse rem) + else + (prerr_endline ("Don't know what to do with " ^ s); usage ()) in try - parse (List.tl (Array.to_list Sys.argv)) + parse arglist with | UserError(_,s) as e -> begin try Stream.empty s; exit 1 with Stream.Failure -> - msgnl (Cerrors.explain_exn e); exit 1 + msgnl (Errors.print e); exit 1 end - | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end + | e -> begin msgnl (Errors.print e); exit 1 end -let init is_ide = +let init arglist = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) Lib.init(); + (* Default Proofb Mode starts with an alternative default. *) + Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic"; begin try - parse_args is_ide; - re_exec is_ide; + let foreign_args = parse_args arglist in + if !filter_opts then + (print_string (String.concat "\n" foreign_args); exit 0); + if !ide_slave then begin + Flags.make_silent true; + Ide_slave.init_stdout () + end; if_verbose print_header (); init_load_path (); inputstate (); @@ -374,13 +351,14 @@ let init is_ide = exit 0); Lib.declare_initial_state () -let init_toplevel () = init false - -let init_ide () = init true; List.rev !ide_args +let init_toplevel = init let start () = - init_toplevel (); - Toplevel.loop(); + init_toplevel (List.tl (Array.to_list Sys.argv)); + if !ide_slave then + Ide_slave.loop () + else + Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); |