]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
Initial revision
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParserContext.ml
index ae21e5d2e0e8193bcd78da63708634e8609cf955..bdf701d8087d5c9640679054edc18fe00ab12422 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-let main ~current_uri ~context lexer lexbuf =
+let main ~current_uri ~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 ;
+ match CicTextualParser.main lexer lexbuf with
+    None -> None
+  | Some res ->
+     CicTextualParser0.binders := [] ;
+     Some (!CicTextualParser0.metasenv,res)
 ;;