Merge PR #1086: [stm] [flags] Move document mode flags to the STM.

4 files changed, 15 insertions, 13 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index d4be81c61a..a178eb7552 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -43,11 +43,8 @@ let with_extra_values o l f x =
 
 let boot = ref false
 let load_init = ref true
-let batch_mode = ref false
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-let compilation_mode = ref BuildVo
-let compilation_output_name = ref None
+let record_aux_file = ref false
 
 let test_mode = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 3024c60396..8ec2a80730 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -13,12 +13,9 @@
 val boot : bool ref
 val load_init : bool ref
 
-(* Will affect STM caching *)
-val batch_mode : bool ref
-
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-val compilation_mode : compilation_mode ref
-val compilation_output_name : string option ref
+(** Set by coqtop to tell the kernel to output to the aux file; will
+    be eventually removed by cleanups such as PR#1103 *)
+val record_aux_file : bool ref
 
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
diff --git a/lib/system.ml b/lib/system.ml
index 0b64b237da..4b5066ef41 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -54,6 +54,8 @@ let make_dir_table dir =
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
   Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
 
+let trust_file_cache = ref true
+
 let exists_in_dir_respecting_case dir bf =
   let cache_dir dir =
     let contents = make_dir_table dir in
@@ -62,10 +64,10 @@ let exists_in_dir_respecting_case dir bf =
   let contents, fresh =
     try
       (* in batch mode, assume the directory content is still fresh *)
-      StrMap.find dir !dirmap, !Flags.batch_mode
+      StrMap.find dir !dirmap, !trust_file_cache
     with Not_found ->
       (* in batch mode, we are not yet sure the directory exists *)
-      if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+      if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true
       else cache_dir dir, true in
   StrSet.mem bf contents ||
     not fresh &&
@@ -80,7 +82,7 @@ let file_exists_respecting_case path f =
     let df = Filename.dirname f in
     (String.equal df "." || aux df)
     && exists_in_dir_respecting_case (Filename.concat path df) bf
-  in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
+  in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f
 
 let rec search paths test =
   match paths with
diff --git a/lib/system.mli b/lib/system.mli
index 7281de97c9..aa964abebe 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -54,6 +54,12 @@ val where_in_path_rex :
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
+val trust_file_cache : bool ref
+(** [trust_file_cache] indicates whether we trust the underlying
+    mapped file-system not to change along the execution of Coq. This
+    assumption greatly speds up file search, but it is often
+    inconvenient in interactive mode *)
+
 val file_exists_respecting_case : string -> string -> bool
 
 (** {6 I/O functions } *)