diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | lib/stateid.ml | 10 | ||||
| -rw-r--r-- | lib/system.ml | 18 | ||||
| -rw-r--r-- | lib/system.mli | 20 |
5 files changed, 27 insertions, 26 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 56940f1cf..7e0065beb 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -57,8 +57,6 @@ let in_toplevel = ref false let profile = false -let ide_slave = ref false - let raw_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 17776d68a..02d8a3adc 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,9 +52,6 @@ val in_toplevel : bool ref val profile : bool -(* -ide_slave: printing will be more verbose, will affect stm caching *) -val ide_slave : bool ref - (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref diff --git a/lib/stateid.ml b/lib/stateid.ml index a258d5052..5485c4bf1 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -11,15 +11,11 @@ type t = int let initial = 1 let dummy = 0 -let fresh, in_range = +let fresh = let cur = ref initial in - (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) + fun () -> incr cur; !cur let to_string = string_of_int -let of_int id = - (* Coqide too to parse ids too, but cannot check if they are valid. - * Hence we check for validity only if we are an ide slave. *) - if !Flags.ide_slave then assert (in_range id); - id +let of_int id = id let to_int id = id let newer_than id1 id2 = id1 > id2 diff --git a/lib/system.ml b/lib/system.ml index dfede29e8..f109c7192 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -116,18 +116,6 @@ let where_in_path ?(warn=true) path filename = let f = Filename.concat lpe filename in if file_exists_respecting_case lpe filename then [lpe,f] else [])) -let where_in_path_rex path rex = - search path (fun lpe -> - try - let files = Sys.readdir lpe in - CList.map_filter (fun name -> - try - ignore(Str.search_forward rex name 0); - Some (lpe,Filename.concat lpe name) - with Not_found -> None) - (Array.to_list files) - with Sys_error _ -> []) - let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then (* the name is considered to be a physical name and we use the file @@ -312,3 +300,9 @@ let with_time ~batch f x = let msg2 = if batch then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e + +let get_toplevel_path top = + let dir = Filename.dirname Sys.argv.(0) in + let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in + let eff = if Dynlink.is_native then ".opt" else ".byte" in + dir ^ Filename.dir_sep ^ top ^ eff ^ exe diff --git a/lib/system.mli b/lib/system.mli index 3349dfea3..a34280037 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -50,8 +50,6 @@ val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string -val where_in_path_rex : - CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string @@ -107,3 +105,21 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b + +(** [get_toplevel_path program] builds a complete path to the + executable denoted by [program]. This involves: + + - locating the directory: we don't rely on PATH as to make calls to + /foo/bin/coqtop chose the right /foo/bin/coqproofworker + + - adding the proper suffixes: .opt/.byte depending on the current + mode, + .exe if in windows. + + Note that this function doesn't check that the executable actually + exists. This is left back to caller, as well as the choice of + fallback strategy. We could add a fallback strategy here but it is + better not to as in most cases if this function fails to construct + the right name you want you execution to fail rather than fall into + choosing some random binary from the system-wide installation of + Coq. *) +val get_toplevel_path : string -> string |