From: Claudio Sacerdoti Coen Date: Tue, 28 Dec 2010 17:21:43 +0000 (+0000) Subject: Useless code removed; interfaces simplified; etc. X-Git-Tag: make_still_working~2617 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79ba29ddfc90c0b9bc26e1ddde46cb94cb800d51;p=helm.git Useless code removed; interfaces simplified; etc. --- diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 11b9d1f52..0bea9c43f 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -45,13 +45,12 @@ let interactive_uri_choice ?copy_cb () ~id uris = - let gui = MatitaMisc.get_gui () in if (selection_mode <> `SINGLE) && (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") then uris else begin - let dialog = gui#newUriDialog () in + let dialog = new uriChoiceDialog () in if hide_uri_entry then dialog#uriEntryHBox#misc#hide (); if hide_try then @@ -326,7 +325,6 @@ let interactive_error_interp ~all_passes (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]])); | _::_ -> let dialog = new disambiguationErrors () in - dialog#check_widgets (); if all_passes then dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false; let model = new interpErrorModel dialog#treeview choices in @@ -430,10 +428,6 @@ class gui () = initializer let s () = MatitaScript.current () in - (* glade's check widgets *) - List.iter (fun w -> w#check_widgets ()) - (let c w = (w :> unit>) in - [ c fileSel; c main; c findRepl]); (* key bindings *) List.iter (* global key bindings *) (fun (key, callback) -> self#addKeyBinding key callback) @@ -1003,23 +997,7 @@ class gui () = let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in closebutton#set_image image#coerce; - let script = - MatitaScript.script - ~urichooser:(fun source_view uris -> - try - interactive_uri_choice ~selection_mode:`SINGLE - ~title:"Matita: URI chooser" - ~msg:"Select the URI" ~hide_uri_entry:true - ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT - ~copy_cb:(fun s -> source_view#buffer#insert ("\n"^s^"\n")) - () ~id:"boh?" uris - with MatitaTypes.Cancel -> []) - ~ask_confirmation: - (fun ~title ~message -> - MatitaGtkMisc.ask_confirmation ~title ~message - ~parent:(MatitaMisc.get_gui ())#main#toplevel ()) - ~parent:scrolledWindow ~tab_label () - in + let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce scrolledWindow#coerce); ignore (closebutton#connect#clicked (fun () -> @@ -1079,28 +1057,12 @@ class gui () = inherit browserWin () val combo = GEdit.entry () initializer - self#check_widgets (); let combo_widget = combo#coerce in uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; combo#misc#grab_focus () method browserUri = combo end - method newUriDialog () = - let dialog = new uriChoiceDialog () in - dialog#check_widgets (); - dialog - - method private newConfirmationDialog () = - let dialog = new confirmationDialog () in - dialog#check_widgets (); - dialog - - method newEmptyDialog () = - let dialog = new emptyDialog () in - dialog#check_widgets (); - dialog - method private addKeyBinding key callback = List.iter (fun evbox -> add_key_binding key callback evbox) keyBindingBoxes @@ -1190,66 +1152,65 @@ class interpModel = let interactive_string_choice text prefix_len ?(title = "") ?(msg = "") () ~id locs uris = - let gui = instance () in - let dialog = gui#newUriDialog () in - dialog#uriEntryHBox#misc#hide (); - dialog#uriChoiceSelectedButton#misc#hide (); - dialog#uriChoiceAutoButton#misc#hide (); - dialog#uriChoiceConstantsButton#misc#hide (); - dialog#uriChoiceTreeView#selection#set_mode - (`SINGLE :> Gtk.Tags.selection_mode); - let model = new stringListModel dialog#uriChoiceTreeView in - let choices = ref None in - dialog#uriChoiceDialog#set_title title; - let hack_len = MatitaGtkMisc.utf8_string_length text in - let rec colorize acc_len = function - | [] -> - let floc = HExtlib.floc_of_loc (acc_len,hack_len) in - escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc)) - | he::tl -> - let start, stop = HExtlib.loc_of_floc he in - let floc1 = HExtlib.floc_of_loc (acc_len,start) in - let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in - let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in - escape_pango_markup str1 ^ "" ^ - escape_pango_markup str2 ^ "" ^ - colorize stop tl - in + let dialog = new uriChoiceDialog () in + dialog#uriEntryHBox#misc#hide (); + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceAutoButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + dialog#uriChoiceTreeView#selection#set_mode + (`SINGLE :> Gtk.Tags.selection_mode); + let model = new stringListModel dialog#uriChoiceTreeView in + let choices = ref None in + dialog#uriChoiceDialog#set_title title; + let hack_len = MatitaGtkMisc.utf8_string_length text in + let rec colorize acc_len = function + | [] -> + let floc = HExtlib.floc_of_loc (acc_len,hack_len) in + escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc)) + | he::tl -> + let start, stop = HExtlib.loc_of_floc he in + let floc1 = HExtlib.floc_of_loc (acc_len,start) in + let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in + let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in + escape_pango_markup str1 ^ "" ^ + escape_pango_markup str2 ^ "" ^ + colorize stop tl + in (* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in - Printf.eprintf "(%d,%d)" start stop) locs; *) - let locs = - List.sort - (fun loc1 loc2 -> - fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) - locs - in + Printf.eprintf "(%d,%d)" start stop) locs; *) + let locs = + List.sort + (fun loc1 loc2 -> + fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) + locs + in (* prerr_endline "XXXXXXXXXXXXXXXXXXXX"; - List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in - Printf.eprintf "(%d,%d)" start stop) locs; - prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *) - dialog#uriChoiceLabel#set_use_markup true; - let txt = colorize 0 locs in - let txt,_ = MatitaGtkMisc.utf8_parsed_text txt - (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) - in - dialog#uriChoiceLabel#set_label txt; - List.iter model#easy_append uris; - let return v = - choices := v; - dialog#uriChoiceDialog#destroy (); - GMain.Main.quit () - in - ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#uriChoiceForwardButton (fun _ -> - match model#easy_selection () with - | [] -> () - | uris -> return (Some uris)); - connect_button dialog#uriChoiceAbortButton (fun _ -> return None); - dialog#uriChoiceDialog#show (); - GtkThread.main (); - (match !choices with - | None -> raise MatitaTypes.Cancel - | Some uris -> uris) + List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) locs; + prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *) + dialog#uriChoiceLabel#set_use_markup true; + let txt = colorize 0 locs in + let txt,_ = MatitaGtkMisc.utf8_parsed_text txt + (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) + in + dialog#uriChoiceLabel#set_label txt; + List.iter model#easy_append uris; + let return v = + choices := v; + dialog#uriChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#uriChoiceForwardButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some uris)); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + dialog#uriChoiceDialog#show (); + GtkThread.main (); + (match !choices with + | None -> raise MatitaTypes.Cancel + | Some uris -> uris) let interactive_interp_choice () text prefix_len choices = (*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*) diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index 2c685c0ad..c9f4f71ff 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -23,17 +23,6 @@ * http://helm.cs.unibo.it/ *) -class type console = -object - method message: string -> unit - method error: string -> unit - method warning: string -> unit - method debug: string -> unit - method clear: unit -> unit - - method log_callback: HLog.log_callback -end - class type browserWin = object inherit MatitaGeneratedGui.browserWin @@ -43,15 +32,12 @@ end class type gui = object (** {2 Access to singleton instances of lower-level GTK widgets} *) - method main : MatitaGeneratedGui.mainWin + method main: MatitaGeneratedGui.mainWin (** {2 Dialogs instantiation} * methods below create a new window on each invocation. You should * remember to destroy windows after use *) - - method newBrowserWin: unit -> browserWin - method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + method newBrowserWin: unit -> browserWin (** {2 Utility methods} *) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index b54d2501c..37e0f9239 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -65,12 +65,7 @@ let first_line s = String.sub s 0 nl_pos with Not_found -> s -type guistuff = { - urichooser: NReference.reference list -> NReference.reference list; - ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; -} - -let eval_with_engine include_paths guistuff status skipped_txt nonskipped_txt st +let eval_with_engine include_paths status skipped_txt nonskipped_txt st = let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt @@ -99,7 +94,7 @@ let eval_with_engine include_paths guistuff status skipped_txt nonskipped_txt st let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let eval_nmacro include_paths (buffer : GText.buffer) guistuff 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) -> @@ -161,23 +156,23 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_t [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length | TA.NAutoInteractive (_, (Some _,_)) -> assert false -let rec eval_executable include_paths (buffer : GText.buffer) guistuff +let rec eval_executable include_paths (buffer : GText.buffer) status unparsed_text skipped_txt nonskipped_txt script ex loc = try ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; - eval_with_engine include_paths guistuff status skipped_txt nonskipped_txt + eval_with_engine include_paths status skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 | GrafiteEngine.NMacro (_loc,macro) -> - eval_nmacro include_paths buffer guistuff status + eval_nmacro include_paths buffer status unparsed_text (skipped_txt ^ nonskipped_txt) script macro -and eval_statement include_paths (buffer : GText.buffer) guistuff status script +and eval_statement include_paths (buffer : GText.buffer) status script statement = let st,unparsed_text = @@ -203,12 +198,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff status script match st with | GrafiteAst.Executable (loc, ex) -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in - eval_executable include_paths buffer guistuff status unparsed_text + 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 - eval_executable include_paths buffer guistuff status unparsed_text + eval_executable include_paths buffer status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, _) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in @@ -216,7 +211,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff status script let s = String.sub unparsed_text parsed_text_length remain_len in let s,text,len = try - eval_statement include_paths buffer guistuff status script (`Raw s) + eval_statement include_paths buffer status script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception @@ -245,7 +240,7 @@ let fresh_script_id = * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may * be added *) -class script ~ask_confirmation ~urichooser ~(parent:GBin.scrolled_window) ~tab_label () = +class script ~(parent:GBin.scrolled_window) ~tab_label () = let source_view = GSourceView2.source_view ~auto_indent:true @@ -297,11 +292,6 @@ object (self) val scriptId = fresh_script_id () - val guistuff = { - urichooser = urichooser source_view; - ask_confirmation = ask_confirmation; - } - val mutable filename_ = (None : string option) method has_name = filename_ <> None @@ -678,7 +668,7 @@ object (self) let time1 = Unix.gettimeofday () in let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff self#status self (`Raw s) + eval_statement self#include_paths buffer self#status self (`Raw s) with End_of_file -> raise Margin in let time2 = Unix.gettimeofday () in @@ -1007,9 +997,9 @@ end let _script = ref [] -let script ~urichooser ~ask_confirmation ~parent ~tab_label () +let script ~parent ~tab_label () = - let s = new script ~ask_confirmation ~urichooser ~parent ~tab_label () in + let s = new script ~parent ~tab_label () in _script := s::!_script; s diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 2152c5eea..9958170d9 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -101,15 +101,7 @@ object end val script: - urichooser: - (GSourceView2.source_view -> NReference.reference list -> - NReference.reference list) -> - ask_confirmation: - (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> - parent:GBin.scrolled_window -> - tab_label:GMisc.label -> - unit -> - script + parent:GBin.scrolled_window -> tab_label:GMisc.label -> unit -> script val destroy: int -> unit val current: unit -> script