diff options
| -rw-r--r-- | dev/doc/build-system.txt | 4 | ||||
| -rw-r--r-- | parsing/cLexer.ml4 | 3 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 6 |
4 files changed, 10 insertions, 5 deletions
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 1c4fd2eba..fd3101613 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -143,7 +143,9 @@ file list(s): These files are also used by the experimental ocamlbuild plugin, which is quite touchy about them : be careful with order, duplicated entries, whitespace errors, and do not mention .mli there. - - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) + If module B depends on module A, then B should be after A in the .mllib + file. +- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget) - The definitions in Makefile.common might have to be adapted too. - If your file needs a specific rule, add it to Makefile.build diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index f26398fa9..52a6fe16c 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -404,8 +404,9 @@ let set_lexer_state (o,s,b,c,f) = between_commands := b; comments := c; current_file := f -let release_lexer_state () = +let get_lexer_state () = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) +let release_lexer_state = get_lexer_state let drop_lexer_state () = set_lexer_state (init_lexer_state Loc.ToplevelInput) diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index d3ef19873..5f4e10f14 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -51,7 +51,9 @@ type lexer_state val init_lexer_state : Loc.source -> lexer_state val set_lexer_state : lexer_state -> unit +val get_lexer_state : unit -> lexer_state val release_lexer_state : unit -> lexer_state +[@@ocaml.deprecated "Use get_lexer_state"] val drop_lexer_state : unit -> unit (* Retrieve the comments lexed at a given location of the stream diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index ddb26d771..7a51908d9 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -111,7 +111,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let state = ref (CLexer.init_lexer_state file) in CLexer.set_lexer_state !state; let a = parsable c in - state := CLexer.release_lexer_state (); + state := CLexer.get_lexer_state (); (a,state) let action = Gramext.action @@ -121,7 +121,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct CLexer.set_lexer_state !state; try let c = Entry.parse e p in - state := CLexer.release_lexer_state (); + state := CLexer.get_lexer_state (); c with Ploc.Exc (loc,e) -> CLexer.drop_lexer_state (); @@ -133,7 +133,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct CLexer.set_lexer_state !state; try let a = f x in - state := CLexer.release_lexer_state (); + state := CLexer.get_lexer_state (); a with e -> CLexer.drop_lexer_state (); |