* 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