X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=c39e1de40a5ec9d9d7856718f196787ba9a4c1b3;hb=e3369ffc8b690703cfafc7985f69db5fc140d749;hp=af3cdf12eb15c7a1381e3e3af84f295838974b20;hpb=423c4e6702b28ae9b017078fb8fcbc7976956318;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index af3cdf12e..c39e1de40 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -26,7 +26,6 @@ (* $Id$ *) open Printf -open GrafiteTypes module TA = GrafiteAst @@ -84,7 +83,7 @@ let eval_with_engine include_paths status skipped_txt nonskipped_txt st (fun (acc, to_prepend) (status,alias) -> match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" - | Some (k,value) -> + | Some (_k,value) -> let newtxt = GrafiteAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment @@ -94,7 +93,7 @@ let eval_with_engine include_paths status skipped_txt nonskipped_txt st let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parsed_text script mac = +let eval_nmacro _include_paths (_buffer : GText.buffer) status _unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in match mac with | TA.Screenshot (_,name) -> @@ -117,11 +116,16 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse 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 @@ -132,7 +136,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse 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 @@ -140,10 +144,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse 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 @@ -153,7 +161,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse 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) @@ -197,12 +205,12 @@ and eval_statement include_paths (buffer : GText.buffer) status script in match st with | GrafiteAst.Executable (loc, ex) -> - let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in eval_executable include_paths buffer status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)) when Helm_registry.get_bool "matita.execcomments" -> - let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in eval_executable include_paths buffer status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, _) -> @@ -242,7 +250,7 @@ let fresh_script_id = *) class script ~(parent:GBin.scrolled_window) ~tab_label () = let source_view = - GSourceView2.source_view + GSourceView3.source_view ~auto_indent:true ~insert_spaces_instead_of_tabs:true ~tab_width:2 ~right_margin_position:80 ~show_right_margin:true @@ -251,34 +259,24 @@ let source_view = () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in +let _ = + source_buffer#connect#notify_can_undo + ~callback:(MatitaMisc.get_gui ())#main#undoMenuItem#misc#set_sensitive in +let _ = + source_buffer#connect#notify_can_redo + ~callback:(MatitaMisc.get_gui ())#main#redoMenuItem#misc#set_sensitive in let similarsymbols_tag_name = "similarsymbolos" in let similarsymbols_tag = `NAME similarsymbols_tag_name 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) @@ -354,7 +352,7 @@ object (self) false )); ignore(source_view#event#connect#button_release - ~callback:(fun button -> clean_locked := false; false)); + ~callback:(fun _button -> clean_locked := false; false)); ignore(source_view#buffer#connect#after#apply_tag ~callback:( fun tag ~start:_ ~stop:_ -> @@ -376,23 +374,21 @@ object (self) let menuItems = menu#children in let undoMenuItem, redoMenuItem = match menuItems with - [undo;redo;sep1;cut;copy;paste;delete;sep2; - selectall;sep3;inputmethod;insertunicodecharacter] -> + [undo;redo;_sep1;cut;copy;paste;delete;_sep2; + _selectall;_sep3;_inputmethod;_insertunicodecharacter] -> List.iter menu#remove [ copy; cut; delete; paste ]; undo,redo | _ -> assert false in let add_menu_item = let i = ref 2 in (* last occupied position *) - fun ?label ?stock () -> + fun ~label -> incr i; - GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i) - () - in - let copy = add_menu_item ~stock:`COPY () in - let cut = add_menu_item ~stock:`CUT () in - let delete = add_menu_item ~stock:`DELETE () in - let paste = add_menu_item ~stock:`PASTE () in - let paste_pattern = add_menu_item ~label:"Paste as pattern" () in + GMenu.menu_item ~label ~packing:(menu#insert ~pos:!i) () in + let copy = add_menu_item ~label:"Copy" in + let cut = add_menu_item ~label:"Cut" in + let delete = add_menu_item ~label:"Delete" in + let paste = add_menu_item ~label:"Paste" in + let paste_pattern = add_menu_item ~label:"Paste as pattern" in copy#misc#set_sensitive self#canCopy; cut#misc#set_sensitive self#canCut; delete#misc#set_sensitive self#canDelete; @@ -404,24 +400,22 @@ object (self) MatitaGtkMisc.connect_menu_item paste self#paste; MatitaGtkMisc.connect_menu_item paste_pattern self#pastePattern; let new_undoMenuItem = - GMenu.image_menu_item - ~image:(GMisc.image ~stock:`UNDO ()) + GMenu.menu_item ~use_mnemonic:true ~label:"_Undo" ~packing:(menu#insert ~pos:0) () in new_undoMenuItem#misc#set_sensitive - (undoMenuItem#misc#get_flag `SENSITIVE); + undoMenuItem#misc#sensitive; menu#remove (undoMenuItem :> GMenu.menu_item); MatitaGtkMisc.connect_menu_item new_undoMenuItem (fun () -> self#safe_undo); let new_redoMenuItem = - GMenu.image_menu_item - ~image:(GMisc.image ~stock:`REDO ()) + GMenu.menu_item ~use_mnemonic:true ~label:"_Redo" ~packing:(menu#insert ~pos:1) () in new_redoMenuItem#misc#set_sensitive - (redoMenuItem#misc#get_flag `SENSITIVE); + redoMenuItem#misc#sensitive; menu#remove (redoMenuItem :> GMenu.menu_item); MatitaGtkMisc.connect_menu_item new_redoMenuItem (fun () -> self#safe_redo))); @@ -787,7 +781,10 @@ 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 @@ -804,6 +801,7 @@ object (self) List.iter (fun o -> o status) observers method activate = + NCicLibrary.replace self#status; self#notify method loadFromFile f = @@ -822,7 +820,7 @@ object (self) 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 = @@ -844,12 +842,12 @@ object (self) 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 =