X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=bf25a5493a75ba8eb0764a9d8ffb6ee32d963d3b;hb=9e8c5d2163e701413517153f00a52dac1cd31ecd;hp=cf141722992e3d49ccba720beba267d0396867d7;hpb=5c56a926588a63ceac31e6ddd6e3eeb02fadf3a9;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index cf1417229..bf25a5493 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -67,8 +67,9 @@ let clean_current_baseuri status = let ask_and_save_moo_if_needed parent fname status = let save () = - MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in - if (MatitaScript.instance ())#eos && + let moo_fname = MatitaMisc.obj_file_of_script fname in + MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in + if (MatitaScript.current ())#eos && status.MatitaTypes.proof_status = MatitaTypes.No_proof then begin @@ -80,7 +81,7 @@ let ask_and_save_moo_if_needed parent fname status = ~title:"A .moo can be generated" ~message:(Printf.sprintf "%s can be generated for %s.\nShould I generate it?" - mooname fname) + (Filename.basename mooname) (Filename.basename fname)) ~parent () in let b = @@ -129,11 +130,6 @@ class gui () = ~default:BuildTimeConf.default_font_size "matita.font_size" in let source_buffer = source_view#source_buffer in -(* let _ = - source_view#event#connect#selection_clear (fun _ -> - prerr_endline "source_view: selection clear"; - false) - in *) object (self) val mutable chosen_file = None val mutable _ok_not_exists = false @@ -176,8 +172,7 @@ class gui () = (*~comments:"comments"*) ~copyright:"Copyright (C) 2005, the HELM team" ~license:(String.concat "\n" (parse_txt_file "LICENSE")) - (*?logo:GdkPixbuf.pixbuf*) - (*?logo_icon_name:string*) + ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png")) ~name:"Matita" ~version:BuildTimeConf.version ~website:"http://helm.cs.unibo.it" @@ -223,7 +218,7 @@ class gui () = let safe_undo = fun () -> (* phase 1: we save the actual status of the marks and we undo *) - let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in + let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in let locked_iter_offset = locked_iter#offset in let mark2 = @@ -251,7 +246,7 @@ class gui () = if mark_iter#offset < locked_iter_offset then begin source_view#buffer#move_mark `INSERT ~where:mark_iter; - (MatitaScript.instance ())#goto `Cursor (); + (MatitaScript.current ())#goto `Cursor (); end; (* phase 4: we perform again the undo. This time we are sure that the text to undo is not locked *) @@ -261,7 +256,7 @@ class gui () = fun () -> (* phase 1: we save the actual status of the marks, we redo and we undo *) - let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in + let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in let locked_iter_offset = locked_iter#offset in let mark2 = @@ -289,7 +284,7 @@ class gui () = if mark_iter#offset < locked_iter_offset then begin source_view#buffer#move_mark `INSERT ~where:mark_iter; - (MatitaScript.instance ())#goto `Cursor (); + (MatitaScript.current ())#goto `Cursor (); end; (* phase 4: we perform again the redo. This time we are sure that the text to redo is not locked *) @@ -357,13 +352,14 @@ class gui () = | Some (s :: _) -> clipboard#set_text s); connect_menu_item main#pasteMenuItem (fun () -> source_view#buffer#paste_clipboard clipboard; - (MatitaScript.instance ())#clean_dirty_lock); + (MatitaScript.current ())#clean_dirty_lock); connect_menu_item main#deleteMenuItem (fun () -> ignore (source_view#buffer#delete_selection ())); connect_menu_item main#selectAllMenuItem (fun () -> source_buffer#move_mark `INSERT source_buffer#start_iter; source_buffer#move_mark `SEL_BOUND source_buffer#end_iter); connect_menu_item main#findReplMenuItem show_find_Repl; + connect_menu_item main#externalEditorMenuItem self#externalEditor; ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = @@ -400,7 +396,7 @@ class gui () = let get_devel_selected () = match model#easy_mselection () with | [[name;_]] -> MatitamakeLib.development_for_name name - | _ -> assert false + | _ -> None in let refresh () = while Glib.Main.pending () do @@ -500,9 +496,9 @@ class gui () = let fname = fileSel#fileSelectionWin#filename in if Sys.file_exists fname then begin - if is_regular fname && not(_only_directory) then + if HExtlib.is_regular fname && not (_only_directory) then return (Some fname) - else if _only_directory && is_dir fname then + else if _only_directory && HExtlib.is_dir fname then return (Some fname) end else @@ -523,15 +519,15 @@ class gui () = (* toolbar *) let module A = GrafiteAst in let hole = CicNotationPt.UserInput in - let loc = Disambiguate.dummy_floc in + let loc = DisambiguateTypes.dummy_floc in let tac ast _ = - if (MatitaScript.instance ())#onGoingProof () then - (MatitaScript.instance ())#advance + if (MatitaScript.current ())#onGoingProof () then + (MatitaScript.current ())#advance ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast))) () in let tac_w_term ast _ = - if (MatitaScript.instance ())#onGoingProof () then + if (MatitaScript.current ())#onGoingProof () then let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ GrafiteAstPp.pp_tactic ast) @@ -540,8 +536,10 @@ class gui () = connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); - connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, []))); - connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, []))); + connect_button tbar#elimButton (tac_w_term + (A.Elim (loc, hole, None, None, []))); + connect_button tbar#elimTypeButton (tac_w_term + (A.ElimType (loc, hole, None, None, []))); connect_button tbar#splitButton (tac (A.Split loc)); connect_button tbar#leftButton (tac (A.Left loc)); connect_button tbar#rightButton (tac (A.Right loc)); @@ -552,7 +550,7 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *) + connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None))); MatitaGtkMisc.toggle_widget_visibility ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) ~check:main#tacticsBarMenuItem; @@ -570,7 +568,10 @@ class gui () = (* log *) MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := - (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn)); + (fun exn -> + if not (Helm_registry.get_bool "matita.debug") then + MatitaLog.error (MatitaExcPp.to_string exn) + else raise exn); (* script *) let _ = match GSourceView.source_language_from_file BuildTimeConf.lang_file with @@ -581,7 +582,7 @@ class gui () = source_buffer#set_language matita_lang; source_buffer#set_highlight true in - let s () = MatitaScript.instance () in + let s () = MatitaScript.current () in let disableSave () = script_fname <- None; main#saveMenuItem#misc#set_sensitive false @@ -608,19 +609,19 @@ class gui () = let script = s () in let status = script#status in try - if source_view#buffer#modified then - begin - match ask_unsaved main#toplevel with - | `YES -> saveScript () - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel - end; - (match script_fname with - | None -> () - | Some fname -> - ask_and_save_moo_if_needed main#toplevel fname status); match self#chooseFile () with | Some f -> + if source_view#buffer#modified then + begin + match ask_unsaved main#toplevel with + | `YES -> saveScript () + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel + end; + (match script_fname with + | None -> () + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname status); script#reset (); script#assignFileName f; source_view#source_buffer#begin_not_undoable_action (); @@ -642,11 +643,11 @@ class gui () = let cursor () = source_buffer#place_cursor (source_buffer#get_iter_at_mark (`NAME "locked")) in - let advance _ = (MatitaScript.instance ())#advance (); cursor () in - let retract _ = (MatitaScript.instance ())#retract (); cursor () in - let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in - let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in - let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in + let advance _ = (MatitaScript.current ())#advance (); cursor () in + let retract _ = (MatitaScript.current ())#retract (); cursor () in + let top _ = (MatitaScript.current ())#goto `Top (); cursor () in + let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in + let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () in let advance = locker (keep_focus advance) in let retract = locker (keep_focus retract) in let top = locker (keep_focus top) in @@ -660,7 +661,7 @@ class gui () = in (* quit *) self#setQuitCallback (fun () -> - let status = (MatitaScript.instance ())#status in + let status = (MatitaScript.current ())#status in if source_view#buffer#modified then begin let rc = ask_unsaved main#toplevel in @@ -733,7 +734,7 @@ class gui () = main#hpaneScriptSequent#set_position script_w; (* source_view *) ignore(source_view#connect#after#paste_clipboard - ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock)); + ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock)); (* clean_locked is set to true only "during" a PRIMARY paste operation (i.e. by clicking with the second mouse button) *) let clean_locked = ref false in @@ -750,11 +751,11 @@ class gui () = ~callback:( fun tag ~start:_ ~stop:_ -> if !clean_locked && - tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid + tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid then begin clean_locked := false; - (MatitaScript.instance ())#clean_dirty_lock; + (MatitaScript.current ())#clean_dirty_lock; clean_locked := true end)); (* math view handling *) @@ -774,8 +775,64 @@ class gui () = MatitaMathView.update_font_sizes ()); MatitaMathView.reset_font_size (); + method private externalEditor () = + let cmd = Helm_registry.get "matita.external_editor" in +(* ZACK uncomment to enable interactive ask of external editor command *) +(* let cmd = + let msg = + "External editor command: +%f will be substitute for the script name, +%p for the cursor position in bytes, +%l for the execution point in bytes." + in + ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false + ~default:(Helm_registry.get "matita.external_editor") () + in *) + let fname = (MatitaScript.current ())#filename in + let slice mark = + source_buffer#start_iter#get_slice + ~stop:(source_buffer#get_iter_at_mark mark) + in + let script = MatitaScript.current () in + let locked = `MARK script#locked_mark in + let string_pos mark = string_of_int (String.length (slice mark)) in + let cursor_pos = string_pos `INSERT in + let locked_pos = string_pos locked in + let cmd = + Pcre.replace ~pat:"%f" ~templ:fname + (Pcre.replace ~pat:"%p" ~templ:cursor_pos + (Pcre.replace ~pat:"%l" ~templ:locked_pos + cmd)) + in + let locked_before = slice locked in + let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in + ignore (Unix.system cmd); + source_buffer#set_text (HExtlib.input_file fname); + let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in + source_buffer#move_mark locked locked_iter; + source_buffer#apply_tag script#locked_tag + ~start:source_buffer#start_iter ~stop:locked_iter; + let locked_after = slice locked in + let line = ref 0 in + let col = ref 0 in + try + for i = 0 to String.length locked_before - 1 do + if locked_before.[i] <> locked_after.[i] then begin + source_buffer#place_cursor + ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col))); + script#goto `Cursor (); + raise Exit + end else if locked_before.[i] = '\n' then begin + incr line; + col := 0 + end + done + with + | Exit -> () + | Invalid_argument _ -> script#goto `Bottom () + method loadScript file = - let script = MatitaScript.instance () in + let script = MatitaScript.current () in script#reset (); script#assignFileName file; let content = @@ -1059,9 +1116,7 @@ let interactive_interp_choice () choices = let selection = dialog#interpChoiceTreeView#selection in ignore (selection#connect#changed (fun _ -> match selection#get_selected_rows with - | [path] -> - MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path)); - interp_no := Some (model#get_interp_no path) + | [path] -> interp_no := Some (model#get_interp_no path) | _ -> assert false)); dialog#interpChoiceDialog#show (); GtkThread.main ();