* so that we can ensure the inclusion is performed after the included file
* is compiled (if needed). matitac does not need that, since it compiles files
* in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths (f : GrafiteParser.statement) x =
+let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x =
try
f ~never_include:true ~include_paths x
with
let ast =
wrap_with_make include_paths
(GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
- (GrafiteTypes.get_lexicon grafite_status)
+ (GrafiteTypes.get_estatus grafite_status)
in
ast, text
- | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text
+ | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text
in
- let grafite_status = GrafiteTypes.set_lexicon lexicon_status grafite_status in
+ let grafite_status = GrafiteTypes.set_estatus lexicon_status grafite_status in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
let source_buffer = source_view#source_buffer in
let initial_statuses baseuri =
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[]
+ CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
BuildTimeConf.core_notation_script
in
let grafite_status = GrafiteSync.init lexicon_status baseuri in
match history with s::_ -> s | [] -> assert false
in
LexiconSync.time_travel
- ~present:(GrafiteTypes.get_lexicon cur_grafite_status)
- ~past:(GrafiteTypes.get_lexicon grafite_status);
+ ~present:(GrafiteTypes.get_estatus cur_grafite_status)
+ ~past:(GrafiteTypes.get_estatus grafite_status);
GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
* library_objects.set_default... *)
GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
LexiconSync.time_travel
- ~present:(GrafiteTypes.get_lexicon self#grafite_status)
- ~past:(GrafiteTypes.get_lexicon grafite_status)
+ ~present:(GrafiteTypes.get_estatus self#grafite_status)
+ ~past:(GrafiteTypes.get_estatus grafite_status)
method private reset_buffer =
statements <- [];
in
try
is_there_only_comments
- (GrafiteTypes.get_lexicon self#grafite_status) self#getFuture
+ (GrafiteTypes.get_estatus self#grafite_status) self#getFuture
with
| LexiconEngine.IncludedFileNotCompiled _
| HExtlib.Localized _