* added popup menu, implemented some functions

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParserContext.ml

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
index ae21e5d2e0e8193bcd78da63708634e8609cf955..6901bd48c28317c262a5444590e31f60cffdf83a 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
@@ -23,11 +23,14 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let main ~current_uri ~context lexer lexbuf =
+let main ~context ~metasenv lexer lexbuf =
  (* Warning: higly non-reentrant code!!! *)
- CicTextualParser0.current_uri := current_uri ;
  CicTextualParser0.binders := context ;
- let res = CicTextualParser.main lexer lexbuf in
-  CicTextualParser0.binders := [] ;
-  res
+ 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
 ;;