Huge reorganization of matita and ocaml.

[helm.git] / helm / ocaml / grafite_parser / cicNotation2.ml

diff --git a/helm/ocaml/grafite_parser/cicNotation2.ml b/helm/ocaml/grafite_parser/cicNotation2.ml
index 2ce3f012f761c43f326446d4dcf4d4d4a5f53e7a..f978f2971f4d5f89d521eb747b09df0cfdbca2ec 100644 (file)
--- a/helm/ocaml/grafite_parser/cicNotation2.ml
+++ b/helm/ocaml/grafite_parser/cicNotation2.ml
@@ -23,47 +23,25 @@
  * http://helm.cs.unibo.it/
  *)
 
-let load_notation fname =
+let load_notation ~include_paths fname =
   let ic = open_in fname in
   let lexbuf = Ulexing.from_utf8_channel ic in
+  let status = ref LexiconSync.init in
   try
-    while true do
-      match GrafiteParser.parse_statement lexbuf with
-      | GrafiteAst.Executable (_, GrafiteAst.Command (_, cmd)) ->
-         ignore (CicNotation.process_notation cmd)
-      | _ -> ()
-    done
-  with End_of_file -> close_in ic
-
-let parse_environment str =
- let stream = Ulexing.from_utf8_string str in
- let environment = ref DisambiguateTypes.Environment.empty in
- let multiple_environment = ref DisambiguateTypes.Environment.empty in
-  try
-    while true do
-     let alias =
-      match GrafiteParser.parse_statement stream with
-         GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias)))
-           -> alias
-       | _ -> assert false in
-     let key,value =
-      (*CSC: Warning: this code should be factorized with the corresponding
-             code in MatitaEngine *)
-      match alias with
-         GrafiteAst.Ident_alias (id,uri) ->
-          DisambiguateTypes.Id id,
-          (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
-       | GrafiteAst.Symbol_alias (symb,instance,desc) ->
-          DisambiguateTypes.Symbol (symb,instance),
-          DisambiguateChoices.lookup_symbol_by_dsc symb desc
-       | GrafiteAst.Number_alias (instance,desc) ->
-          DisambiguateTypes.Num instance,
-          DisambiguateChoices.lookup_num_by_dsc desc
-     in
-      environment := DisambiguateTypes.Environment.add key value !environment;
-      multiple_environment := DisambiguateTypes.Environment.cons key value !multiple_environment;
-    done;
-    assert false
-  with End_of_file ->
-   !environment, !multiple_environment
+   while true do
+    status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status)
+   done;
+   assert false
+  with End_of_file -> close_in ic; !status
 
+let parse_environment ~include_paths str =
+ let lexbuf = Ulexing.from_utf8_string str in
+ let status = ref LexiconSync.init in
+ try
+  while true do
+   status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status)
+  done;
+  assert false
+ with End_of_file ->
+  !status.LexiconEngine.aliases,
+  !status.LexiconEngine.multi_aliases