diff options
| -rw-r--r-- | lib/aux_file.ml | 2 | ||||
| -rw-r--r-- | lib/aux_file.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 22 |
3 files changed, 21 insertions, 7 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c9018c9ee..5dedb0d0a 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -42,6 +42,8 @@ module M = Map.Make(String) type data = string M.t type aux_file = data H.t +let contents x = x + let empty_aux_file = H.empty let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) diff --git a/lib/aux_file.mli b/lib/aux_file.mli index e340fc654..b672d3db2 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string val empty_aux_file : aux_file val set : aux_file -> Loc.t -> string -> string -> aux_file +module H : Map.S with type key = int * int +module M : Map.S with type key = string +val contents : aux_file -> string M.t H.t + val start_aux_file_for : string -> unit val stop_aux_file : unit -> unit val recording : unit -> bool diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 72c800f0f..6f1ed85e0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1846,8 +1846,9 @@ let vernac_load interp fname = (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility *) -let interp ?proof locality poly c = + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let interp ?proof ~loc locality poly c = prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) @@ -1991,10 +1992,16 @@ let interp ?proof locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no" + | VernacProof (Some tac, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no"; + vernac_set_end_tac tac + | VernacProof (None, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes"; + vernac_set_used_variables l | VernacProof (Some tac, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes"; vernac_set_end_tac tac; vernac_set_used_variables l | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) @@ -2146,8 +2153,9 @@ let interp ?(verbosely=true) ?proof (loc,c) = Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> - if verbosely then Flags.verbosely (interp ?proof locality poly) c - else Flags.silently (interp ?proof locality poly) c; + if verbosely + then Flags.verbosely (interp ?proof ~loc locality poly) c + else Flags.silently (interp ?proof ~loc locality poly) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode end |