X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=d4157677feabd3573bae00edf5c4d84d52795c3d;hb=6fa89cef6aa8fc1774db065a9fcfc47867579054;hp=e0ca8c6816fb88b97bc00e59d7f0122adf408f15;hpb=29a5b18f3da1a3ed648f23709384b7789cb099bf;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index e0ca8c681..d4157677f 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -67,13 +67,14 @@ 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 = MatitacleanLib.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 let mooname = - MatitaMisc.obj_file_of_script fname + MatitacleanLib.obj_file_of_script fname in let rc = MatitaGtkMisc.ask_confirmation @@ -217,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 = @@ -245,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 *) @@ -255,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 = @@ -283,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 *) @@ -351,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 _ = @@ -394,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 @@ -494,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 @@ -519,13 +521,13 @@ class gui () = let hole = CicNotationPt.UserInput 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) @@ -548,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))); + connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None))); MatitaGtkMisc.toggle_widget_visibility ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) ~check:main#tacticsBarMenuItem; @@ -567,7 +569,7 @@ class gui () = MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := (fun exn -> - if Helm_registry.get_bool "matita.catch_top_level_exn" then + if not (Helm_registry.get_bool "matita.debug") then MatitaLog.error (MatitaExcPp.to_string exn) else raise exn); (* script *) @@ -580,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 @@ -641,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 @@ -659,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 @@ -732,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 @@ -749,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 *) @@ -773,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 = @@ -824,8 +882,8 @@ class gui () = dialog#check_widgets (); dialog - method newInterpDialog () = - let dialog = new interpChoiceDialog () in + method newRecordDialog () = + let dialog = new recordChoiceDialog () in dialog#check_widgets (); dialog @@ -1037,30 +1095,30 @@ class interpModel = let interactive_interp_choice () choices = let gui = instance () in assert (choices <> []); - let dialog = gui#newInterpDialog () in - let model = new interpModel dialog#interpChoiceTreeView choices in + let dialog = gui#newRecordDialog () in + let model = new interpModel dialog#recordChoiceTreeView choices in let interp_len = List.length (List.hd choices) in - dialog#interpChoiceDialog#set_title "Interpretation choice"; - dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:"; + dialog#recordChoiceDialog#set_title "Interpretation choice"; + dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:"; let interp_no = ref None in let return _ = - dialog#interpChoiceDialog#destroy (); + dialog#recordChoiceDialog#destroy (); GMain.Main.quit () in let fail _ = interp_no := None; return () in - ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#interpChoiceOkButton (fun _ -> + ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#recordChoiceOkButton (fun _ -> match !interp_no with None -> () | Some _ -> return ()); - connect_button dialog#interpChoiceCancelButton fail; - ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ -> + connect_button dialog#recordChoiceCancelButton fail; + ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ -> interp_no := Some (model#get_interp_no path); return ())); - let selection = dialog#interpChoiceTreeView#selection in + let selection = dialog#recordChoiceTreeView#selection in ignore (selection#connect#changed (fun _ -> match selection#get_selected_rows with | [path] -> interp_no := Some (model#get_interp_no path) | _ -> assert false)); - dialog#interpChoiceDialog#show (); + dialog#recordChoiceDialog#show (); GtkThread.main (); (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)