From 834b2ded0b9db67e0a19139546ac1f267de5544f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Jan 2004 15:12:11 +0000 Subject: [PATCH] The parser have been made more functional with a trick. Now there is no more need to save and restore the metasenv. --- .../cic_textual_parser/cicTextualParserContext.ml | 12 +++++++----- .../texCicTextualParserContext.ml | 12 +++++++----- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml index 6901bd48c..c9dfe664b 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml +++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml @@ -28,9 +28,11 @@ let main ~context ~metasenv lexer lexbuf = CicTextualParser0.binders := context ; CicTextualParser0.metasenv := metasenv ; let dom,mk_term = CicTextualParser.main lexer lexbuf in - dom, - function interp -> - let term = mk_term interp in - let metasenv = !CicTextualParser0.metasenv in - metasenv,term + let metasenv' = !CicTextualParser0.metasenv in + dom, + function interp -> + CicTextualParser0.metasenv := metasenv' ; + let term = mk_term interp in + let metasenv = !CicTextualParser0.metasenv in + metasenv,term ;; diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml index 28581bc58..e14259589 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml @@ -28,9 +28,11 @@ let main ~context ~metasenv lexer lexbuf = TexCicTextualParser0.binders := context ; TexCicTextualParser0.metasenv := metasenv ; let dom,mk_term = TexCicTextualParser.main lexer lexbuf in - dom, - function interp -> - let term = mk_term interp in - let metasenv = !TexCicTextualParser0.metasenv in - metasenv,term + let metasenv' = !TexCicTextualParser0.metasenv in + dom, + function interp -> + TexCicTextualParser0.metasenv := metasenv' ; + let term = mk_term interp in + let metasenv = !TexCicTextualParser0.metasenv in + metasenv,term ;; -- 2.39.2