diff options
Diffstat (limited to 'parsing/cLexer.ml4')
| -rw-r--r-- | parsing/cLexer.ml4 | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 52a6fe16c..d65b35c46 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -384,16 +386,6 @@ let comments = ref [] let current_comment = Buffer.create 8192 let between_commands = ref true -let rec split_comments comacc acc pos = function - [] -> comments := List.rev acc; comacc - | ((b,e),c as com)::coms -> - (* Take all comments that terminates before pos, or begin exactly - at pos (used to print comments attached after an expression) *) - if e<=pos || pos=b then split_comments (c::comacc) acc pos coms - else split_comments comacc (com::acc) pos coms - -let extract_comments pos = split_comments [] [] pos !comments - (* The state of the lexer visible from outside *) type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source @@ -410,6 +402,8 @@ let release_lexer_state = get_lexer_state let drop_lexer_state () = set_lexer_state (init_lexer_state Loc.ToplevelInput) +let get_comment_state (_,_,_,c,_) = c + let real_push_char c = Buffer.add_char current_comment c (* Add a char if it is between two commands, if it is a newline or |