diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-11 12:58:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 20:14:13 +0200 |
| commit | 4e31561f7e0d5e647e86978806cae82ffb35f90b (patch) | |
| tree | ca7f7540c690bd40c5e29fcd3c8cde7c257ff9a6 /toplevel | |
| parent | e4fcf8f9af193f125eb6ee101e739ba4460bd8b8 (diff) | |
Removing export of location_table outside of cLexer.
It was not used any more by coqdoc since b8194b22 (Dec 2010).
The table is now only part of the lexer function closure
(and only in the camlp5 case).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 19 |
2 files changed, 7 insertions, 14 deletions
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 |