aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml474
-rw-r--r--parsing/cLexer.mli8
-rw-r--r--parsing/compat.ml476
3 files changed, 110 insertions, 48 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index f19759470..a7b413f57 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,34 +340,46 @@ let comm_loc bp = match !comment_begin with
| None -> comment_begin := Some bp
| _ -> ()
-let current = Buffer.create 8192
-let between_com = ref true
-
-type com_state = int option * string * bool
-let restore_com_state (o,s,b) =
+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
+
+type comments_state = int option * string * bool * ((int * int) * string) list
+let restore_comments_state (o,s,b,c) =
comment_begin := o;
- Buffer.clear current; Buffer.add_string current s;
- between_com := b
-let dflt_com = (None,"",true)
-let com_state () =
- let s = (!comment_begin, Buffer.contents current, !between_com) in
- restore_com_state dflt_com; s
+ Buffer.clear current_comment; Buffer.add_string current_comment s;
+ between_commands := b;
+ comments := c
+let default_comments_state = (None,"",true,[])
+let comments_state () =
+ let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in
+ restore_comments_state default_comments_state; s
-let real_push_char c = Buffer.add_char current 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
if the last char is not a space itself. *)
let push_char c =
if
- !between_com || List.mem c ['\n';'\r'] ||
+ !between_commands || List.mem c ['\n';'\r'] ||
(List.mem c [' ';'\t']&&
- (Int.equal (Buffer.length current) 0 ||
- not (let s = Buffer.contents current in
+ (Int.equal (Buffer.length current_comment) 0 ||
+ not (let s = Buffer.contents current_comment in
List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r'])))
then
real_push_char c
-let push_string s = Buffer.add_string current s
+let push_string s = Buffer.add_string current_comment s
let null_comment s =
let rec null i =
@@ -375,12 +387,12 @@ let null_comment s =
null (String.length s - 1)
let comment_stop ep =
- let current_s = Buffer.contents current in
- if !Flags.xml_export && Buffer.length current > 0 &&
- (!between_com || not(null_comment current_s)) then
+ let current_s = Buffer.contents current_comment in
+ if !Flags.xml_export && Buffer.length current_comment > 0 &&
+ (!between_commands || not(null_comment current_s)) then
Hook.get f_xml_output_comment current_s;
- (if Flags.do_beautify() && Buffer.length current > 0 &&
- (!between_com || not(null_comment current_s)) then
+ (if Flags.do_beautify() && Buffer.length current_comment > 0 &&
+ (!between_commands || not(null_comment current_s)) then
let bp = match !comment_begin with
Some bp -> bp
| None ->
@@ -389,10 +401,10 @@ let comment_stop ep =
++ str current_s ++str"' ending at "
++ int ep);
ep-1 in
- Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
- Buffer.clear current;
+ comments := ((bp,ep),current_s) :: !comments);
+ Buffer.clear current_comment;
comment_begin := None;
- between_com := false
+ between_commands := false
(* Does not unescape!!! *)
let rec comm_string loc bp = parser
@@ -548,16 +560,16 @@ let rec next_token loc = parser bp
| KEYWORD ("." | "...") ->
if not (blank_or_eof s) then
err (set_loc_pos loc bp (ep+1)) Undefined_token;
- between_com := true;
+ between_commands := true;
| _ -> ()
in
(t, set_loc_pos loc bp ep)
| [< ' ('-'|'+'|'*' as c); s >] ->
- let t,new_between_com =
- if !between_com then process_sequence loc bp c s, true
+ let t,new_between_commands =
+ if !between_commands then process_sequence loc bp c s, true
else process_chars loc bp c s,false
in
- comment_stop bp; between_com := new_between_com; t
+ comment_stop bp; between_commands := new_between_commands; t
| [< ''?'; s >] ep ->
let t = parse_after_qmark loc bp s in
comment_stop bp; (t, set_loc_pos loc ep bp)
@@ -590,9 +602,9 @@ let rec next_token loc = parser bp
(try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep
| AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) ->
let t = process_chars loc bp (Stream.next s) s in
- let new_between_com = match t with
- (KEYWORD ("{"|"}"),_) -> !between_com | _ -> false in
- comment_stop bp; between_com := new_between_com; t
+ let new_between_commands = match t with
+ (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in
+ comment_stop bp; between_commands := new_between_commands; t
| EmptyStream ->
comment_stop bp; (EOI, set_loc_pos loc bp (bp+1))
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 3b4891d9a..3ad49eb74 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -34,12 +34,12 @@ type frozen_t
val freeze : unit -> frozen_t
val unfreeze : frozen_t -> unit
-type com_state
-val com_state: unit -> com_state
-val restore_com_state: com_state -> unit
-
val xml_output_comment : (string -> unit) Hook.t
+(* Retrieve the comments lexed at a given location of the stream
+ currently being processeed *)
+val extract_comments : int -> string list
+
val terminal : string -> Tok.t
(** The lexer of Coq: *)
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 389c34fa5..58b74da26 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -138,12 +138,21 @@ module type LexerSig = sig
exception E of t
val to_string : t -> string
end
+ type comments_state
+ val default_comments_state : comments_state
+ val comments_state : unit -> comments_state
+ val restore_comments_state : comments_state -> unit
end
ELSE
-module type LexerSig =
- Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+module type LexerSig = sig
+ include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+ type comments_state
+ val default_comments_state : comments_state
+ val comments_state : unit -> comments_state
+ val restore_comments_state : comments_state -> unit
+end
END
@@ -162,10 +171,13 @@ module type GrammarSig = sig
string option * Gramext.g_assoc option * production_rule list
type extend_statment =
Gramext.position option * single_extend_statment list
+ type coq_parsable
+ val parsable : char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
- val entry_parse : 'a entry -> parsable -> 'a
+ val entry_parse : 'a entry -> coq_parsable -> 'a
val entry_print : Format.formatter -> 'a entry -> unit
+ val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
val srules' : production_rule list -> symbol
val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
end
@@ -181,14 +193,33 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
string option * Gramext.g_assoc option * production_rule list
type extend_statment =
Gramext.position option * single_extend_statment list
+ type coq_parsable = parsable * L.comments_state ref
+ let parsable c =
+ let state = ref L.default_comments_state in (parsable c, state)
let action = Gramext.action
let entry_create = Entry.create
- let entry_parse e p =
- try Entry.parse e p
+ let entry_parse e (p,state) =
+ L.restore_comments_state !state;
+ try
+ let c = Entry.parse e p in
+ state := L.comments_state ();
+ L.restore_comments_state L.default_comments_state;
+ c
with Exc_located (loc,e) ->
+ L.restore_comments_state L.default_comments_state;
let loc' = Loc.get_loc (Exninfo.info e) in
let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
Loc.raise ~loc e
+ let with_parsable (p,state) f x =
+ L.restore_comments_state !state;
+ try
+ let a = f x in
+ state := L.comments_state ();
+ L.restore_comments_state L.default_comments_state;
+ a
+ with e ->
+ L.restore_comments_state L.default_comments_state;
+ raise e
let entry_print ft x = Entry.print ft x
let srules' = Gramext.srules
@@ -202,12 +233,13 @@ module type GrammarSig = sig
with module Loc = CompatLoc and type Token.t = Tok.t
type 'a entry = 'a Entry.t
type action = Action.t
- type parsable
- val parsable : char Stream.t -> parsable
+ type coq_parsable
+ val parsable : char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
- val entry_parse : 'a entry -> parsable -> 'a
+ val entry_parse : 'a entry -> coq_parsable -> 'a
val entry_print : Format.formatter -> 'a entry -> unit
+ val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
val srules' : production_rule list -> symbol
end
@@ -217,13 +249,31 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
include Camlp4.Struct.Grammar.Static.Make (L)
type 'a entry = 'a Entry.t
type action = Action.t
- type parsable = char Stream.t
- let parsable s = s
+ type comments_state = int option * string * bool * ((int * int) * string) list
+ type coq_parsable = char Stream.t * L.comments_state ref
+ let parsable s = let state = ref L.default_comments_state in (s, state)
let action = Action.mk
let entry_create = Entry.mk
- let entry_parse e s =
- try parse e (*FIXME*)CompatLoc.ghost s
- with Exc_located (loc,e) -> raise_coq_loc loc e
+ let entry_parse e (s,state) =
+ L.restore_comments_state !state;
+ try
+ let c = parse e (*FIXME*)CompatLoc.ghost s in
+ state := L.comments_state ();
+ L.restore_comments_state L.default_comments_state;
+ c
+ with Exc_located (loc,e) ->
+ L.restore_comments_state L.default_comments_state;
+ raise_coq_loc loc e
+ let with_parsable (p,state) f x =
+ L.restore_comments_state !state;
+ try
+ let a = f x in
+ state := L.comments_state ();
+ L.restore_comments_state L.default_comments_state;
+ a
+ with e ->
+ L.restore_comments_state L.default_comments_state;
+ raise e
let entry_print ft x = Entry.print ft x
let srules' = srules (entry_create "dummy")
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 19:21:43 +0000