X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=94e3e751db0f046b2f27cf01f36ca761b8fb202e;hb=3c8da07d7a5d7cf0432a83732a6d103f527afaef;hp=489afc2838507c3c4b0fd5ada1f0dd21664a995e;hpb=4b3a9a15edbab7a3aa819155dc1ac1eec1ddb0a3;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 489afc283..94e3e751d 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -35,8 +35,6 @@ exception Found of int let all_disambiguation_passes = ref false -let gui_instance = ref None - (* this is a shit and should be changed :-{ *) let interactive_uri_choice ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") @@ -45,13 +43,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 @@ -107,14 +104,6 @@ let interactive_uri_choice end -class type browserWin = - (* this class exists only because GEdit.combo_box_entry is not supported by - * lablgladecc :-(((( *) -object - inherit MatitaGeneratedGui.browserWin - method browserUri: GEdit.entry -end - class console ~(buffer: GText.buffer) () = object (self) val error_tag = buffer#create_tag [ `FOREGROUND "red" ] @@ -136,18 +125,22 @@ class console ~(buffer: GText.buffer) () = | `Warning -> self#warning (s ^ "\n") end -let clean_current_baseuri grafite_status = - LibraryClean.clean_baseuris [grafite_status#baseuri] +let clean_current_baseuri status = + LibraryClean.clean_baseuris [status#baseuri] -let save_moo grafite_status = - let script = MatitaScript.current () in - let baseuri = grafite_status#baseuri in +let save_moo0 ~do_clean script status = + let baseuri = status#baseuri in match script#bos, script#eos with | true, _ -> () | _, true -> GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - grafite_status - | _ -> clean_current_baseuri grafite_status + status + | _ -> if do_clean then clean_current_baseuri status +;; + +let save_moo status = + let script = MatitaScript.current () in + save_moo0 ~do_clean:true script status ;; let ask_unsaved parent filename = @@ -326,7 +319,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 @@ -427,23 +419,24 @@ class gui () = val mutable chosen_file = None val mutable _ok_not_exists = false val mutable _only_directory = false + val mutable current_page = -1 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) + (fun (key, modifiers, callback) -> + self#addKeyBinding key ~modifiers callback) (* [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, toggle_win ~check:main#showCheckMenuItem check#checkWin; *) - [ ]; + [ + GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page; + GdkKeysyms._Page_Up, [`CONTROL], main#scriptNotebook#previous_page + ]; (* about win *) let parse_txt_file file = let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in @@ -605,7 +598,7 @@ class gui () = match !id with | None -> assert false (* a race condition occurred *) | Some id -> - (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id)); + source_view#source_buffer#misc#disconnect id)); source_view#source_buffer#place_cursor (source_view#source_buffer#get_iter (`OFFSET x')); end; @@ -768,8 +761,7 @@ class gui () = MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem ~callback:(function b -> let s = s () in - let status = - Interpretations.toggle_active_interpretations s#grafite_status b + let _status = Interpretations.toggle_active_interpretations s#status b in assert false (* MATITA 1.0 ??? s#set_grafite_status status*) @@ -782,7 +774,7 @@ class gui () = main#unicodeAsTexMenuItem#set_active (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) - HLog.set_log_callback self#console#log_callback; + HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg); GtkSignal.user_handler := (function | MatitaScript.ActionCancelled s -> HLog.error s @@ -840,23 +832,15 @@ class gui () = connect_menu_item main#saveAsMenuItem (fun () -> self#saveAsScript (MatitaScript.current ())); connect_menu_item main#newMenuItem self#newScript; - connect_menu_item main#closeMenuItem self#closeScript; + connect_menu_item main#closeMenuItem self#closeCurrentScript; connect_menu_item main#showCoercionsGraphMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Coercions)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions))); connect_menu_item main#showHintsDbMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Hints)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints))); connect_menu_item main#showTermGrammarMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Grammar)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar))); connect_menu_item main#showUnicodeTable - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `TeX)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX))); (* debug menu *) main#debugMenu#misc#hide (); (* HBUGS *) @@ -879,18 +863,19 @@ class gui () = main#hpaneScriptSequent#set_position script_w; (* math view handling *) connect_menu_item main#newCicBrowserMenuItem (fun () -> - ignore(MatitaMathView.cicBrowser ())); + ignore(MatitaMathView.cicBrowser None)); connect_menu_item main#increaseFontSizeMenuItem MatitaMisc.increase_font_size; connect_menu_item main#decreaseFontSizeMenuItem MatitaMisc.decrease_font_size; connect_menu_item main#normalFontSizeMenuItem MatitaMisc.reset_font_size; - ignore (main#scriptNotebook#connect#switch_page - (fun page -> - let script = MatitaScript.at_page page in - script#activate; - main#saveMenuItem#misc#set_sensitive script#has_name)); + ignore (main#scriptNotebook#connect#switch_page (fun page -> + self#save_page (); + current_page <- page; + let script = MatitaScript.at_page page in + script#activate; + main#saveMenuItem#misc#set_sensitive script#has_name)) method private externalEditor () = let script = MatitaScript.current () in @@ -973,57 +958,61 @@ class gui () = with | `YES -> self#saveScript script; - save_moo script#grafite_status; + save_moo script#status; true | `NO -> true | `CANCEL -> false else - (save_moo script#grafite_status; true) + (save_moo script#status; true) - method private closeScript () = - let page = main#scriptNotebook#current_page in - let script = MatitaScript.at_page page in + method private closeScript page script = if self#closeScript0 script then begin MatitaScript.destroy page; ignore (main#scriptNotebook#remove_page page) end + method private closeCurrentScript () = + let page = main#scriptNotebook#current_page in + let script = MatitaScript.at_page page in + self#closeScript page script + + method private save_page () = + if current_page >= 0 then + let old_script = MatitaScript.at_page current_page in + save_moo0 ~do_clean:false old_script old_script#status + method newScript () = + self#save_page (); let scrolledWindow = GBin.scrolled_window () in - let tab_label = GMisc.label ~text:"foo" () in - 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 - ignore (main#scriptNotebook#prepend_page ~tab_label:tab_label#coerce scrolledWindow#coerce); + let hbox = GPack.hbox () in + let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in + let _ = + GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in + let closebutton = + GButton.button ~relief:`NONE ~packing:hbox#pack () in + let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in + closebutton#set_image image#coerce; + 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 () -> + self#closeScript + (main#scriptNotebook#page_num scrolledWindow#coerce) script)); main#scriptNotebook#goto_page 0; sequents_viewer#reset; sequents_viewer#load_logo; let browser_observer _ = MatitaMathView.refresh_all_browsers () in - let sequents_observer grafite_status = + let sequents_observer status = sequents_viewer#reset; - match grafite_status#ng_mode with + match status#ng_mode with `ProofMode -> - sequents_viewer#nload_sequents grafite_status; + sequents_viewer#nload_sequents status; (try let goal = - Continuationals.Stack.find_goal grafite_status#stack + Continuationals.Stack.find_goal status#stack in - sequents_viewer#goto_sequent grafite_status goal + sequents_viewer#goto_sequent status goal with Failure _ -> ()); | `CommandMode -> sequents_viewer#load_logo in @@ -1060,35 +1049,9 @@ class gui () = method private findRepl = findRepl method main = main - method newBrowserWin () = - object (self) - 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) + method private addKeyBinding key ?modifiers callback = +(* List.iter (fun evbox -> add_key_binding key callback evbox) *) + List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback) keyBindingBoxes method private setQuitCallback callback = @@ -1116,9 +1079,10 @@ class gui () = let gui () = let g = new gui () in - gui_instance := Some g; - MatitaMisc.set_gui g; - g + let rg = (g :> MatitaGuiTypes.gui) in + MatitaMisc.set_gui rg; + g#newScript (); + rg let instance = singleton gui @@ -1176,66 +1140,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;*)