Avoid race conditions (deadlocks)

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 33296d2320ec2be4487110090af548ba9586d86b..711ac975a8482b0b10993aaf87b141150148cdb3 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -26,7 +26,6 @@
 (* $Id$ *)
 
 open Printf
-open GrafiteTypes
 
 module TA = GrafiteAst
 
@@ -84,7 +83,7 @@ let eval_with_engine include_paths status skipped_txt nonskipped_txt st
       (fun (acc, to_prepend) (status,alias) ->
        match alias with
        | None -> (status,to_prepend ^ nonskipped_txt)::acc,""
-       | Some (k,value) ->
+       | Some (_k,value) ->
             let newtxt = GrafiteAstPp.pp_alias value in
             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
       ([],skipped_txt) enriched_history_fragment
@@ -94,7 +93,7 @@ let eval_with_engine include_paths status skipped_txt nonskipped_txt st
 
 let pp_eager_statement_ast = GrafiteAstPp.pp_statement 
 
-let eval_nmacro include_paths (buffer : GText.buffer) 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) -> 
@@ -103,7 +102,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
        let name = Filename.dirname (script#filename) ^ "/" ^ name in
        let sequents = 
          let selected = Continuationals.Stack.head_goals status#stack in
-         List.filter (fun x,_ -> List.mem x selected) menv         
+         List.filter (fun (x,_) -> List.mem x selected) menv         
        in
        CicMathView.screenshot status sequents menv subst name;
        [status, parsed_text], "", parsed_text_length
@@ -206,12 +205,12 @@ and eval_statement include_paths (buffer : GText.buffer) status script
   in 
   match st with
   | GrafiteAst.Executable (loc, ex) ->
-     let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
+     let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in
       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
+     let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in
       eval_executable include_paths buffer status unparsed_text
        skipped nonskipped script ex loc
   | GrafiteAst.Comment (loc, _) -> 
@@ -271,7 +270,7 @@ let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
  let status = new MatitaEngine.status baseuri in
  (match current with
-     Some current -> NCicLibrary.time_travel status;
+     Some _current -> NCicLibrary.time_travel status;
 (*
       (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate () *)
@@ -353,7 +352,7 @@ object (self)
           false
         ));
     ignore(source_view#event#connect#button_release
-      ~callback:(fun button -> clean_locked := false; false));
+      ~callback:(fun _button -> clean_locked := false; false));
     ignore(source_view#buffer#connect#after#apply_tag
      ~callback:(
        fun tag ~start:_ ~stop:_ ->
@@ -375,8 +374,8 @@ object (self)
        let menuItems = menu#children in
        let undoMenuItem, redoMenuItem =
         match menuItems with
-           [undo;redo;sep1;cut;copy;paste;delete;sep2;
-            selectall;sep3;inputmethod;insertunicodecharacter] ->
+           [undo;redo;_sep1;cut;copy;paste;delete;_sep2;
+            _selectall;_sep3;_inputmethod;_insertunicodecharacter] ->
               List.iter menu#remove [ copy; cut; delete; paste ];
               undo,redo
          | _ -> assert false in
@@ -774,7 +773,8 @@ object (self)
       | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
     in
     buffer#move_mark mark ~where:new_mark_pos;
-    buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
+    (* CSC: the next line is required to avoid race conditions (deadlocks) *)
+    GtkThread.sync(fun () -> buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos) ();
     buffer#move_mark `INSERT old_insert;
     let mark_position = buffer#get_iter_at_mark mark in
     if source_view#move_mark_onscreen mark then