diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 61 | ||||
| -rw-r--r-- | stm/stm.mli | 46 |
3 files changed, 53 insertions, 56 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fd689602df..9eb0924bd6 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -372,7 +372,7 @@ module Make(T : Task) () = struct let with_n_workers n priority f = let q = create n priority in try let rc = f q in destroy q; rc - with e -> let e = CErrors.push e in destroy q; iraise e + with e -> let e = Exninfo.capture e in destroy q; Exninfo.iraise e let n_workers { active } = Pool.n_workers active diff --git a/stm/stm.ml b/stm/stm.ml index 95c58b9043..a5b868343d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1014,7 +1014,7 @@ end = struct (* {{{ *) if PG_compat.there_are_pending_proofs () then VCS.goals id (PG_compat.get_open_goals ()) with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let good_id = !cur_id in invalidate_cur_state (); VCS.reached id; @@ -1046,7 +1046,7 @@ end = struct (* {{{ *) unfreeze st; res with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Vernacstate.invalidate_cache (); unfreeze st; Exninfo.iraise e @@ -1540,7 +1540,7 @@ end = struct (* {{{ *) RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with @@ -1687,7 +1687,7 @@ end = struct (* {{{ *) `OK proof end with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (try match Stateid.get info with | None -> msg_warning Pp.( @@ -2092,7 +2092,7 @@ end = struct (* {{{ *) ignore(stm_vernac_interp r_for st { r_what with verbose = true }); feedback ~id:r_for Processed with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let msg = iprint e in feedback ~id:r_for (Message (Error, None, msg)) @@ -2337,7 +2337,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = else try f () with e when CErrors.noncritical e -> - let ie = CErrors.push e in + let ie = Exninfo.capture e in error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = @@ -2435,7 +2435,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Stateid.add info ~valid:prev id in Exninfo.iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () @@ -2569,28 +2569,32 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initialization routine *) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) - (* Require [require_libs] before the initial state is + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] is used. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } + + (* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = @@ -2615,7 +2619,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } = let require_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in @@ -2633,7 +2637,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Loadpath.add_coq_path iload_path; + List.iter Mltop.add_ml_dir ml_load_path; + List.iter Loadpath.add_vo_path vo_load_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -2688,7 +2693,7 @@ let observe ~doc id = VCS.print (); doc with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in VCS.print (); VCS.restore vcs; Exninfo.iraise e @@ -2763,7 +2768,7 @@ let finish_tasks name u p (t,rcbackup as tasks) = let a, _ = List.fold_left finish_task u (info_tasks tasks) in (a,true), p with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 @@ -2987,7 +2992,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.print (); rc with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in handle_failure e vcs let get_ast ~doc id = @@ -3197,7 +3202,7 @@ let edit_at ~doc id = VCS.print (); doc, rc with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in match Stateid.get info with | None -> VCS.print (); diff --git a/stm/stm.mli b/stm/stm.mli index 841adcf05b..e56bac6e0f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,38 +52,30 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initialization options: - - - [doc_type]: Type of document being created. - - - [require_libs]: list of libraries/modules to be pre-loaded at - startup. A tuple [(modname,modfrom,import)] is equivalent to [From - modfrom Require modname]; [import] works similarly to - [Library.require_library_from_dirpath], [Some false] will import - the module, [Some true] will additionally export it. - -*) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; - - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; - - (* Require [require_libs] before the initial state is +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) + + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) + + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] is used. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } (** The type of a STM document *) type doc |