The OK button of the disambiguation errors interface now adds aliases to the

current script. However, the aliases are used only in passes 1 and 3 :-(

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index c718bd81a8353ef44d1afafa2f87019e4c2a812d..ff00ce27b69d925cc125a1220149cd9614a211a4 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -232,8 +232,7 @@ class interpErrorModel =
     end
 
 
-let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn
- offset errorll
+let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
 = 
   let errorll' =
    if all_passes then errorll else
@@ -314,37 +313,69 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn
        dialog#disambiguationErrors#set_title "Disambiguation error";
        dialog#disambiguationErrorsLabel#set_label
         "Click on an error to see the corresponding message:";
-       ignore (dialog#treeview#connect#cursor_changed (fun _ ->
-        let tree_path =
-         match fst (dialog#treeview#get_cursor ()) with
-            None -> assert false
-         | Some tp -> tp in
-        let idx1,idx2,idx3 = model#get_interp_no tree_path in
-        let loffset,lll = List.nth choices idx1 in
-        let _,envs_and_diffs,msg =
-         match idx2 with
-            Some idx2 -> List.nth lll idx2
-          | None -> [],[],lazy "Multiple error messages. Please select one." in
-        let _,env,diff =
-         match idx3 with
-            Some idx3 -> List.nth envs_and_diffs idx3
-          | None -> [],[],[] (* dymmy value, used *) in
-        let script = MatitaScript.current () in
-        let error_tag = script#error_tag in
-         source_buffer#remove_tag error_tag
-           ~start:source_buffer#start_iter
-           ~stop:source_buffer#end_iter;
-         notify_exn
-          (GrafiteDisambiguator.DisambiguationError
-            (offset,[[env,diff,loffset,msg]]))
-         ));
+       ignore (dialog#treeview#connect#cursor_changed
+        (fun _ ->
+          let tree_path =
+           match fst (dialog#treeview#get_cursor ()) with
+              None -> assert false
+           | Some tp -> tp in
+          let idx1,idx2,idx3 = model#get_interp_no tree_path in
+          let loffset,lll = List.nth choices idx1 in
+          let _,envs_and_diffs,msg =
+           match idx2 with
+              Some idx2 -> List.nth lll idx2
+            | None -> [],[],lazy "Multiple error messages. Please select one." in
+          let _,env,diff =
+           match idx3 with
+              Some idx3 -> List.nth envs_and_diffs idx3
+            | None -> [],[],[] (* dymmy value, used *) in
+          let script = MatitaScript.current () in
+          let error_tag = script#error_tag in
+           source_buffer#remove_tag error_tag
+             ~start:source_buffer#start_iter
+             ~stop:source_buffer#end_iter;
+           notify_exn
+            (GrafiteDisambiguator.DisambiguationError
+              (offset,[[env,diff,loffset,msg]]))
+           ));
        let return _ =
          dialog#disambiguationErrors#destroy ();
          GMain.Main.quit ()
        in
        let fail _ = return () in
-       ignore (dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
-       connect_button dialog#disambiguationErrorsOkButton (fun _ -> return ());
+       ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
+       connect_button dialog#disambiguationErrorsOkButton
+        (fun _ ->
+          let tree_path =
+           match fst (dialog#treeview#get_cursor ()) with
+              None -> assert false
+           | Some tp -> tp in
+          let idx1,idx2,idx3 = model#get_interp_no tree_path in
+          let diff =
+           match idx2,idx3 with
+              Some idx2, Some idx3 ->
+               let _,lll = List.nth choices idx1 in
+               let _,envs_and_diffs,_ = List.nth lll idx2 in
+               let _,_,diff = List.nth envs_and_diffs idx3 in
+                diff
+            | _,_ -> assert false
+          in
+           let newtxt =
+            String.concat "\n"
+             ("" ::
+               List.map
+                (fun k,value ->
+                  DisambiguatePp.pp_environment
+                   (DisambiguateTypes.Environment.add k value
+                     DisambiguateTypes.Environment.empty))
+                diff) ^ "\n"
+           in
+            source_buffer#insert
+             ~iter:
+               (source_buffer#get_iter_at_mark
+                (`NAME "beginning_of_statement")) newtxt ;
+            return ()
+        );
        connect_button dialog#disambiguationErrorsMoreErrors
         (fun _ -> return () ;
           interactive_error_interp ~all_passes:true source_buffer notify_exn offset

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 23de391c6ed37e486d1b0324f429325a41d98af4..0e51213096292c4caf09b2b93058fbf024f8e169 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -363,6 +363,9 @@ script ex loc
            | `CANCEL -> raise MatitaTypes.Cancel)
      | _ -> ()
    end;
+   ignore (buffer#move_mark (`NAME "beginning_of_statement")
+    ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
+       (Glib.Utf8.length skipped_txt))) ;
    eval_with_engine
     guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
      (TA.Executable (loc, ex))
@@ -501,6 +504,9 @@ object (self)
   (** text mark and tag representing locked part of a script *)
   val locked_mark =
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
+  val beginning_of_statement_mark =
+    buffer#create_mark ~name:"beginning_of_statement"
+     ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]