aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/cLexer.ml459
-rw-r--r--parsing/cLexer.mli4
-rw-r--r--parsing/compat.ml476
-rw-r--r--toplevel/coqloop.ml12
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/vernac.ml29
-rw-r--r--toplevel/vernac.mli4
7 files changed, 116 insertions, 70 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index bec891f7f1..777cdc9bf7 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -340,34 +340,35 @@ let comm_loc bp = match !comment_begin with
| None -> comment_begin := Some bp
| _ -> ()
-let current = Buffer.create 8192
-let between_com = ref true
+let current_comment = Buffer.create 8192
+let between_commands = ref true
-type com_state = int option * string * bool
-let restore_com_state (o,s,b) =
+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;
+ Pp.comments := c
+let default_comments_state = (None,"",true,[])
+let comments_state () =
+ let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !Pp.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 +376,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 ->
@@ -390,9 +391,9 @@ let comment_stop ep =
++ int ep);
ep-1 in
Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
- Buffer.clear current;
+ 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 +549,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 +591,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 3b4891d9ac..2c05d6a95f 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -34,10 +34,6 @@ 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
val terminal : string -> Tok.t
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 18bc8d664f..ecf515111c 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
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 69d68bd357..bdcfa8336d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
mutable str : string; (* buffer of already read characters *)
mutable len : int; (* number of chars in the buffer *)
mutable bols : int list; (* offsets in str of beginning of lines *)
- mutable tokens : Gram.parsable; (* stream of tokens *)
+ mutable tokens : Gram.coq_parsable; (* stream of tokens *)
mutable start : int } (* stream count of the first char of the buffer *)
(* Double the size of the buffer. *)
@@ -274,10 +274,12 @@ let rec discard_to_dot () =
| End_of_input -> raise End_of_input
| e when CErrors.noncritical e -> ()
-let read_sentence () =
+let read_eval_sentence () =
try
- let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
- CWarnings.set_current_loc loc; r
+ let input = (top_buffer.tokens, None) in
+ let (loc, _ as r) = Vernac.parse_sentence input in
+ CWarnings.set_current_loc loc;
+ Vernac.eval_expr input r
with reraise ->
let reraise = CErrors.push reraise in
discard_to_dot ();
@@ -298,7 +300,7 @@ let do_vernac () =
if !print_emacs then top_stderr (str (top_buffer.prompt()));
resynch_buffer top_buffer;
try
- Vernac.eval_expr (read_sentence ())
+ read_eval_sentence ()
with
| End_of_input | CErrors.Quit ->
top_stderr (fnl ()); raise CErrors.Quit
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 00554da308..e40353e0f9 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
mutable str : string; (** buffer of already read characters *)
mutable len : int; (** number of chars in the buffer *)
mutable bols : int list; (** offsets in str of begining of lines *)
- mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *)
+ mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
mutable start : int } (** stream count of the first char of the buffer *)
(** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bdd834d52f..5db6042371 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,7 +124,7 @@ let set_formatter_translator() =
Format.set_formatter_output_functions out (fun () -> flush ch);
Format.set_max_boxes max_int
-let pr_new_syntax loc ocom =
+let pr_new_syntax_in_context loc ocom =
let loc = Loc.unloc loc in
if !beautify_file then set_formatter_translator();
let fs = States.freeze ~marshallable:`No in
@@ -138,20 +138,20 @@ let pr_new_syntax loc ocom =
States.unfreeze fs;
Format.set_formatter_out_channel stdout
+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
- let cl = !Pp.comments in
- let cs = CLexer.com_state() in
(* end translator state *)
let coqdocstate = CLexer.location_table () in
- ch,cl,cs,coqdocstate
+ ch,coqdocstate
-let restore_translator_coqdoc (ch,cl,cs,coqdocstate) =
+let restore_translator_coqdoc (ch,coqdocstate) =
if !Flags.beautify_file then close_out !chan_beautify;
chan_beautify := ch;
- Pp.comments := cl;
- CLexer.restore_com_state cs;
CLexer.restore_location_table coqdocstate
(* For coqtop -time, we display the position in the file,
@@ -182,7 +182,7 @@ let print_cmd_header loc com =
Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com);
Format.pp_print_flush !Pp_control.std_ft ()
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com input checknav (loc,com) =
let interp = function
| VernacLoad (verbosely, fname) ->
let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -194,7 +194,6 @@ let rec vernac_com checknav (loc,com) =
if !Flags.beautify_file then
begin
chan_beautify := open_out (f^beautify_suffix);
- Pp.comments := []
end;
begin
try
@@ -214,13 +213,11 @@ let rec vernac_com checknav (loc,com) =
in
try
checknav loc com;
- if do_beautify () then pr_new_syntax loc (Some com);
+ if do_beautify () then pr_new_syntax input loc (Some com);
(* XXX: This is not 100% correct if called from an IDE context *)
if !Flags.time then print_cmd_header loc com;
let com = if !Flags.time then VernacTime (loc,com) else com in
- let a = CLexer.com_state () in
- interp com;
- CLexer.restore_com_state a
+ interp com
with reraise ->
let (reraise, info) = CErrors.push reraise in
Format.set_formatter_out_channel stdout;
@@ -240,7 +237,7 @@ and read_vernac_file verbosely s =
while true do
let loc_ast = parse_sentence input in
CWarnings.set_current_loc (fst loc_ast);
- vernac_com checknav loc_ast;
+ vernac_com input checknav loc_ast;
done
with any -> (* whatever the exception *)
let (e, info) = CErrors.push any in
@@ -249,7 +246,7 @@ and read_vernac_file verbosely s =
match e with
| End_of_input ->
if do_beautify () then
- pr_new_syntax (Loc.make_loc (max_int,max_int)) None
+ pr_new_syntax input (Loc.make_loc (max_int,max_int)) None
| reraise ->
iraise (disable_drop e, info)
@@ -264,7 +261,7 @@ let checknav loc ast =
if is_deep_navigation_vernac ast then
user_error loc "Navigation commands forbidden in nested commands"
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr input loc_ast = vernac_com input checknav loc_ast
(* XML output hooks *)
let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 7bfddd9470..2fd86ddc22 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -11,7 +11,7 @@
(** Read a vernac command on the specified input (parse only).
Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
-val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
+val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
Loc.t * Vernacexpr.vernac_expr
(** Reads and executes vernac commands from a stream.
@@ -21,7 +21,7 @@ exception End_of_input
val just_parsing : bool ref
-val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit
(** Set XML hooks *)
val xml_start_library : (unit -> unit) Hook.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 09:08:49 +0000