diff options
| -rw-r--r-- | parsing/cLexer.ml4 | 8 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 19 |
4 files changed, 7 insertions, 30 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 181c4b7fd..0090117f6 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -626,12 +626,6 @@ let loct_func loct i = let loct_add loct i loc = Hashtbl.add loct i loc -let current_location_table = ref (loct_create ()) - -type location_table = (int, Compat.CompatLoc.t) Hashtbl.t -let location_table () = !current_location_table -let restore_location_table t = current_location_table := t - (** {6 The lexer of Coq} *) (** Note: removing a token. @@ -669,7 +663,6 @@ let func cs = cur_loc := Compat.after loc; loct_add loct i loc; Some tok) in - current_location_table := loct; (ts, loct_func loct) let lexer = { @@ -706,7 +699,6 @@ end let mk () = let loct = loct_create () in let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in - current_location_table := loct; let rec self init_loc (* FIXME *) = parser i [< (tok, loc) = next_token !cur_loc; s >] -> diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 3ad49eb74..71edda760 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -10,14 +10,6 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool -(* val location_function : int -> Loc.t *) - -(** for coqdoc *) -type location_table -val location_table : unit -> location_table -val restore_location_table : location_table -> unit - - (** [get_current_file fname] returns the filename used in locations emitted by the lexer *) val get_current_file : unit -> string diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7a67e0951..26ef68262 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -228,11 +228,9 @@ let compile_files () = if !compile_list == [] then () else let init_state = States.freeze ~marshallable:`No in - let coqdoc_init_state = CLexer.location_table () in Feedback.(add_feeder debug_feeder); List.iter (fun vf -> States.unfreeze init_state; - CLexer.restore_location_table coqdoc_init_state; compile_file vf) (List.rev !compile_list) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b8e44db9a..661a597ae 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -145,17 +145,12 @@ let pr_new_syntax (po,_) loc ocom = (* Reinstall the context of parsing which includes the bindings of comments to locations *) Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom -let save_translator_coqdoc () = - (* translator state *) - let ch = !chan_beautify in - (* end translator state *) - let coqdocstate = CLexer.location_table () in - ch,coqdocstate +let save_translator () = + !chan_beautify -let restore_translator_coqdoc (ch,coqdocstate) = +let restore_translator ch = if !Flags.beautify_file then close_out !chan_beautify; - chan_beautify := ch; - CLexer.restore_location_table coqdocstate + chan_beautify := ch (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) @@ -191,7 +186,7 @@ let rec vernac_com input checknav (loc,com) = let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - let st = save_translator_coqdoc () in + let st = save_translator () in let old_lexer_file = CLexer.get_current_file () in CLexer.set_current_file f; if !Flags.beautify_file then @@ -201,11 +196,11 @@ let rec vernac_com input checknav (loc,com) = begin try Flags.silently (read_vernac_file verbosely) f; - restore_translator_coqdoc st; + restore_translator st; CLexer.set_current_file old_lexer_file; with reraise -> let reraise = CErrors.push reraise in - restore_translator_coqdoc st; + restore_translator st; CLexer.set_current_file old_lexer_file; iraise reraise end |