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
let s = NTactics.intros_tac ~names_ref [] script#status in
let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
- [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+ [s, nl ^ "#" ^ String.concat " #" !names_ref], "", parsed_text_length
| TA.NAutoInteractive (_loc, (None,a)) ->
let trace_ref = ref [] in
let s = NnAuto.auto_tac ~params:(None,a) ~trace_ref script#status in
try List.assoc "depth" a
with Not_found -> ""
in
- let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+ let width =
+ try List.assoc "width" a
+ with Not_found -> ""
+ in
+ let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in
let thms =
match !trace_ref with
- | [] -> "{}"
+ | [] -> ""
| thms ->
String.concat ", "
(HExtlib.filter_map (function
in
let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
- [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+ [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
let rec eval_executable include_paths (buffer : GText.buffer)
~insert_spaces_instead_of_tabs:true ~tab_width:2
~right_margin_position:80 ~show_right_margin:true
~smart_home_end:`AFTER
- ~packing:parent#add_with_viewport
+ ~packing:parent#add
() in
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses current baseuri =
let status = new MatitaEngine.status baseuri in
(match current with
- Some current ->
- NCicLibrary.time_travel status;
+ Some current -> NCicLibrary.time_travel status;
(*
(* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
NCicEnvironment.invalidate () *)
| None -> ());
status
in
-let read_include_paths file =
- try
- let root, _buri, _fname, _tgt =
- Librarian.baseuri_of_script ~include_paths:[] file in
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- let rc = root :: includes in
- List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
- []
-in
let default_buri = "cic:/matita/tests" in
let default_fname = ".unnamed.ma" in
object (self)
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
List.iter (fun o -> o status) observers
method activate =
+ NCicLibrary.replace self#status;
self#notify
method loadFromFile f =
let f = Librarian.absolutize file in
tab_label#set_text (Filename.basename f);
filename_ <- Some f;
- include_paths_ <- read_include_paths f;
+ include_paths_ <- MatitaEngine.read_include_paths ~include_paths:[] f;
self#reset_buffer
method set_star b =
method private _saveToBackupFile () =
if buffer#modified then
begin
- let f = self#filename in
+ let f = self#filename ^ "~" in
let oc = open_out f in
output_string oc (buffer#get_text ~start:buffer#start_iter
~stop:buffer#end_iter ());
close_out oc;
- HLog.debug ("backup " ^ f ^ " saved")
+ HLog.debug ("backup " ^ f ^ " saved")
end
method private reset_buffer =