if tl <> [] then
HLog.warn
"Many goals focused. Using the context of the first one\n";
- let _, ctx, _ = NCicUtils.lookup_meta g menv in
- ctx in
+ let ctx = try
+ let _, ctx, _ = NCicUtils.lookup_meta g menv in ctx
+ with NCicUtils.Meta_not_found _ ->
+ HLog.warn "Current goal is closed. Using empty context.";
+ [ ]
+ in ctx
+ in
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
- status None ctx menv subst (parsed_text,parsed_text_length,
+ status `XTNone ctx menv subst (parsed_text,parsed_text_length,
NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
buffer#move_mark mark mark_position;
source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
end;
- while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+ let time0 = Unix.gettimeofday () in
+ GtkThread.sync (fun () -> while Glib.Main.pending () do ignore(Glib.Main.iteration false); done) ();
+ let time1 = Unix.gettimeofday () in
+ HLog.debug ("... refresh done in " ^ string_of_float (time1 -. time0) ^ "s")
method clean_dirty_lock =
let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in