X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=bf25a5493a75ba8eb0764a9d8ffb6ee32d963d3b;hb=9e8c5d2163e701413517153f00a52dac1cd31ecd;hp=8351426f88702e4191141634596cafd1c2323c6a;hpb=5b17a67ffd16485adf2e66a6241b72e91ed15621;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 8351426f8..bf25a5493 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -69,7 +69,7 @@ let ask_and_save_moo_if_needed parent fname status =
   let save () =
     let moo_fname = MatitaMisc.obj_file_of_script fname in
     MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
-  if (MatitaScript.instance ())#eos &&
+  if (MatitaScript.current ())#eos &&
      status.MatitaTypes.proof_status = MatitaTypes.No_proof
   then
     begin
@@ -218,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 =
@@ -246,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 *)
@@ -256,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 =
@@ -284,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 *)
@@ -352,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 _ =
@@ -520,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)
@@ -568,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 *)
@@ -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
@@ -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 =