X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParserContext.ml;h=c9dfe664b2f9f20666a45466c561c9c701f50a07;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=bdf701d8087d5c9640679054edc18fe00ab12422;hpb=faf328f5779a7281c9c0588680b1b7bb89ae7640;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
index bdf701d80..c9dfe664b 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
@@ -23,14 +23,16 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let main ~current_uri ~context ~metasenv lexer lexbuf =
+let main ~context ~metasenv lexer lexbuf =
  (* Warning: higly non-reentrant code!!! *)
- CicTextualParser0.current_uri := current_uri ;
  CicTextualParser0.binders := context ;
  CicTextualParser0.metasenv := metasenv ;
- match CicTextualParser.main lexer lexbuf with
-    None -> None
-  | Some res ->
-     CicTextualParser0.binders := [] ;
-     Some (!CicTextualParser0.metasenv,res)
+ let dom,mk_term = CicTextualParser.main lexer lexbuf in
+  let metasenv' = !CicTextualParser0.metasenv in
+   dom,
+    function interp ->
+     CicTextualParser0.metasenv := metasenv' ;
+     let term = mk_term interp in 
+     let metasenv = !CicTextualParser0.metasenv in
+      metasenv,term
 ;;