aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml429
-rw-r--r--parsing/cLexer.mli8
-rw-r--r--parsing/compat.ml479
3 files changed, 56 insertions, 60 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 0090117f6..cfee77ab2 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -101,14 +101,6 @@ module Error = struct
end
open Error
-let current_file = ref ""
-
-let get_current_file () =
- !current_file
-
-let set_current_file ~fname =
- current_file := fname
-
let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str)
let bad_token str = raise (Error.E (Bad_token str))
@@ -334,6 +326,9 @@ let rec string loc ~comm_level bp len = parser
(* Hook for exporting comment into xml theory files *)
let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
+(* To associate locations to a file name *)
+let current_file = ref None
+
(* Utilities for comments in beautify *)
let comment_begin = ref None
let comm_loc bp = match !comment_begin with
@@ -354,16 +349,20 @@ let rec split_comments comacc acc pos = function
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) =
+(* The state of the lexer visible from outside *)
+type lexer_state = int option * string * bool * ((int * int) * string) list * string option
+
+let init_lexer_state f = (None,"",true,[],f)
+let set_lexer_state (o,s,b,c,f) =
comment_begin := o;
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
+ comments := c;
+ current_file := f
+let release_lexer_state () =
+ (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+let drop_lexer_state () =
+ set_lexer_state (init_lexer_state None)
let real_push_char c = Buffer.add_char current_comment c
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 71edda760..f69d95335 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
-(** [get_current_file fname] returns the filename used in locations emitted by
- the lexer *)
-val get_current_file : unit -> string
-
-(** [set_current_file fname] sets the filename used in locations emitted by the
- lexer *)
-val set_current_file : fname:string -> unit
-
val check_ident : string -> unit
val is_ident : string -> bool
val check_keyword : string -> unit
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 26e07c2f2..befa0d01b 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -10,6 +10,10 @@
(** Locations *)
+let file_loc_of_file = function
+| None -> ""
+| Some f -> f
+
IFDEF CAMLP5 THEN
module CompatLoc = struct
@@ -29,7 +33,7 @@ let to_coqloc loc =
Loc.line_nb_last = Ploc.line_nb_last loc;
Loc.bol_pos_last = Ploc.bol_pos_last loc; }
-let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc fname line_nb bol_pos (bp, ep) ""
+let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
(* Update a loc without allocating an intermediate pair *)
let set_loc_pos loc bp ep =
@@ -80,7 +84,7 @@ let to_coqloc loc =
Loc.bol_pos_last = CompatLoc.stop_bol loc; }
let make_loc fname line_nb bol_pos start stop =
- CompatLoc.of_tuple (fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
+ CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
open CompatLoc
@@ -97,7 +101,7 @@ let bump_loc_line_last loc bol_pos =
stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
let set_loc_file loc fname =
- of_tuple (fname, start_line loc, start_bol loc, start_off loc,
+ of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc,
stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
let after loc =
@@ -138,20 +142,22 @@ 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
+ type lexer_state
+ val init_lexer_state : string option -> lexer_state
+ val set_lexer_state : lexer_state -> unit
+ val release_lexer_state : unit -> lexer_state
+ val drop_lexer_state : unit -> unit
end
ELSE
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
+ type lexer_state
+ val init_lexer_state : string option -> lexer_state
+ val set_lexer_state : lexer_state -> unit
+ val release_lexer_state : unit -> lexer_state
+ val drop_lexer_state : unit -> unit
end
END
@@ -172,7 +178,7 @@ module type GrammarSig = sig
type extend_statment =
Gramext.position option * single_extend_statment list
type coq_parsable
- val parsable : char Stream.t -> coq_parsable
+ val parsable : ?file:string -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -193,32 +199,34 @@ 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)
+ type coq_parsable = parsable * L.lexer_state ref
+ let parsable ?file c =
+ let state = ref (L.init_lexer_state file) in
+ L.set_lexer_state !state;
+ let a = parsable c in
+ state := L.release_lexer_state ();
+ (a,state)
let action = Gramext.action
let entry_create = Entry.create
let entry_parse e (p,state) =
- L.restore_comments_state !state;
+ L.set_lexer_state !state;
try
let c = Entry.parse e p in
- state := L.comments_state ();
- L.restore_comments_state L.default_comments_state;
+ state := L.release_lexer_state ();
c
with Exc_located (loc,e) ->
- L.restore_comments_state L.default_comments_state;
+ L.drop_lexer_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;
+ L.set_lexer_state !state;
try
let a = f x in
- state := L.comments_state ();
- L.restore_comments_state L.default_comments_state;
+ state := L.release_lexer_state ();
a
with e ->
- L.restore_comments_state L.default_comments_state;
+ L.drop_lexer_state ();
raise e
let entry_print ft x = Entry.print ft x
@@ -234,7 +242,7 @@ module type GrammarSig = sig
type 'a entry = 'a Entry.t
type action = Action.t
type coq_parsable
- val parsable : char Stream.t -> coq_parsable
+ val parsable : ?file:string -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -249,31 +257,28 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
include Camlp4.Struct.Grammar.Static.Make (L)
type 'a entry = 'a Entry.t
type action = Action.t
- 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)
+ type coq_parsable = char Stream.t * L.lexer_state ref
+ let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state)
let action = Action.mk
let entry_create = Entry.mk
let entry_parse e (s,state) =
- L.restore_comments_state !state;
+ L.set_lexer_state !state;
try
let c = parse e (*FIXME*)CompatLoc.ghost s in
- state := L.comments_state ();
- L.restore_comments_state L.default_comments_state;
+ state := L.release_lexer_state ();
c
with Exc_located (loc,e) ->
- L.restore_comments_state L.default_comments_state;
- raise_coq_loc loc e
+ L.drop_lexer_state ();
+ raise_coq_loc loc e;;
let with_parsable (p,state) f x =
- L.restore_comments_state !state;
+ L.set_lexer_state !state;
try
let a = f x in
- state := L.comments_state ();
- L.restore_comments_state L.default_comments_state;
+ state := L.release_lexer_state ();
a
with e ->
- L.restore_comments_state L.default_comments_state;
- Pervasives.raise e
+ L.drop_lexer_state ();
+ Pervasives.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-30 09:35:30 +0000