X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=cf1c0de4df94a203ac73c6ea0ab04be63e8c0642;hb=f9512e878bd27f8cb5261bb18b0da0d42c8184d0;hp=b230adecc50f41ae68cb8c22c3facd47b25ac30d;hpb=679f6296c9a979213425104fa606809d9f1e3bad;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index b230adecc..cf1c0de4d 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -129,6 +129,127 @@ let ask_unsaved parent =
          "<i>Do you want to save the script before continuing?</i>")
     ()
 
+class interpErrorModel =
+  let cols = new GTree.column_list in
+  let id_col = cols#add Gobject.Data.string in
+  let dsc_col = cols#add Gobject.Data.string in
+  let interp_no_col = cols#add Gobject.Data.int in
+  let tree_store = GTree.tree_store cols in
+  let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
+  let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
+  let id_view_col = GTree.view_column ~renderer:id_renderer () in
+  let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
+  fun tree_view choices ->
+    object
+      initializer
+        tree_view#set_model (Some (tree_store :> GTree.model));
+        ignore (tree_view#append_column id_view_col);
+        ignore (tree_view#append_column dsc_view_col);
+        tree_store#clear ();
+        let idx = ref ~-1 in
+        List.iter
+          (fun passes,env,_,_,_ ->
+            incr idx;
+            let interp_row = tree_store#append () in
+            tree_store#set ~row:interp_row ~column:id_col
+              ("Passes " ^ String.concat " " (List.map string_of_int passes));
+            tree_store#set ~row:interp_row ~column:interp_no_col !idx;
+            List.iter
+              (fun (_, id, dsc) ->
+                let row = tree_store#append ~parent:interp_row () in
+                tree_store#set ~row ~column:id_col id;
+                tree_store#set ~row ~column:dsc_col dsc;
+                tree_store#set ~row ~column:interp_no_col !idx)
+              env)
+          choices
+
+      method get_interp_no tree_path =
+        let iter = tree_store#get_iter tree_path in
+        tree_store#get ~row:iter ~column:interp_no_col
+    end
+
+
+let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn
+ offset errorll
+= 
+  let errorll' =
+   if all_passes then errorll else List.rev (List.tl (List.tl (List.rev errorll))) in
+  let choices =
+   let pass = ref 0 in
+   List.flatten
+    (List.map
+      (fun l ->
+        incr pass;
+        List.map
+         (fun (env,diff,offset,msg) -> [!pass], env, diff, offset, msg) l
+      ) errorll') in
+  (* Here we are doing a stable sort and list_uniq returns the latter
+     "equal" element. I.e. we are showing the error corresponding to the
+     most advanced disambiguation pass *)
+  let choices =
+   let choices_compare (_,e1,_,_,m1) (_,e2,_,_,m2) =
+    let m1 = Lazy.force m1 in
+    let m2 = Lazy.force m2 in
+     compare (e1,m1) (e2,m2) in
+   let choices_compare_by_passes (p1,_,_,_,_) (p2,_,_,_,_) = compare p1 p2 in
+   let rec uniq =
+    function
+       [] -> []
+     | h::[] -> [h]
+     | (p1,e1,_,_,_)::(p2,e2,d2,o2,m2)::tl when e1 = e2 ->
+         uniq ((p1@p2,e2,d2,o2,m2) :: tl) 
+     | h1::tl -> h1 :: uniq tl
+   in
+    List.sort choices_compare_by_passes
+     (uniq (List.stable_sort choices_compare choices))
+  in
+   match choices with
+      [] -> assert false
+    | [_,env,diff,loffset,msg] ->
+        notify_exn
+         (GrafiteDisambiguator.DisambiguationError
+           (offset,[[env,diff,loffset,msg]]));
+    | _::_ ->
+       let dialog = new disambiguationErrors () in
+       dialog#check_widgets ();
+       if all_passes then
+        dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+       let model = new interpErrorModel dialog#treeview choices in
+       dialog#disambiguationErrors#set_title "Disambiguation error";
+       dialog#disambiguationErrorsLabel#set_label
+        "Click on an interpretation to see the corresponding error 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 idx = model#get_interp_no tree_path in
+        let _,env,diff,loffset,msg = List.nth choices idx 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 ());
+       connect_button dialog#disambiguationErrorsMoreErrors
+        (fun _ -> return () ;
+          interactive_error_interp ~all_passes:true source_buffer notify_exn offset
+           errorll);
+       connect_button dialog#disambiguationErrorsCancelButton fail;
+       dialog#disambiguationErrors#show ();
+       GtkThread.main ()
+
+
 (** Selection handling
  * Two clipboards are used: "clipboard" and "primary".
  * "primary" is used by X, when you hit the middle button mouse is content is
@@ -415,17 +536,83 @@ class gui () =
       let lock_world _ =
         main#buttonsToolbar#misc#set_sensitive false;
         develList#buttonsHbox#misc#set_sensitive false;
+        main#scriptMenu#misc#set_sensitive false;
         source_view#set_editable false
       in
       let unlock_world _ =
         main#buttonsToolbar#misc#set_sensitive true;
         develList#buttonsHbox#misc#set_sensitive true;
-        source_view#set_editable true
+        main#scriptMenu#misc#set_sensitive true;
+        source_view#set_editable true;
+        (*The next line seems sufficient to avoid some unknown race condition *)
+        GtkThread.sync (fun () -> ()) ()
       in
-      let locker f = 
+      let worker_thread = ref None in
+      let notify_exn exn =
+       let floc, msg = MatitaExcPp.to_string exn in
+        begin
+         match floc with
+            None -> ()
+          | Some floc ->
+             let (x, y) = HExtlib.loc_of_floc floc in
+             let script = MatitaScript.current () in
+             let locked_mark = script#locked_mark in
+             let error_tag = script#error_tag in
+             let baseoffset =
+              (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
+             let x' = baseoffset + x in
+             let y' = baseoffset + y in
+             let x_iter = source_buffer#get_iter (`OFFSET x') in
+             let y_iter = source_buffer#get_iter (`OFFSET y') in
+             source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+             let id = ref None in
+             id := Some (source_buffer#connect#changed ~callback:(fun () ->
+               source_buffer#remove_tag error_tag
+                 ~start:source_buffer#start_iter
+                 ~stop:source_buffer#end_iter;
+               match !id with
+               | None -> assert false (* a race condition occurred *)
+               | Some id ->
+                   (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
+             source_buffer#place_cursor
+              (source_buffer#get_iter (`OFFSET x'));
+        end;
+        HLog.error msg in
+      let locker f () =
+       let thread_main =
         fun () -> 
           lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+          try
+           f ();
+           unlock_world ()
+          with
+           | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+              interactive_error_interp source_buffer notify_exn offset errorll ;
+              unlock_world ()
+           | exc ->
+              notify_exn exc;
+              unlock_world ()
+       in
+        worker_thread := Some (Thread.create thread_main ()) in
+      let kill_worker =
+       (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
+       let interrupt = ref None in
+       let old_callback = ref (function _ -> ()) in
+       let force_interrupt n =
+         (* This function is called just before the thread's timeslice ends *)
+         !old_callback n;
+         if Some(Thread.id(Thread.self())) = !interrupt then
+          (interrupt := None; raise Sys.Break) in
+       let _ =
+        match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with
+           Sys.Signal_handle f -> old_callback := f
+         | Sys.Signal_ignore
+         | Sys.Signal_default -> assert false
+       in
+        fun () ->
+         match !worker_thread with
+            None -> assert false
+          | Some t -> interrupt := Some (Thread.id t) in
       let keep_focus f =
         fun () ->
          try
@@ -486,10 +673,19 @@ class gui () =
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
-              let clean = locker 
-                (fun () -> MatitamakeLib.publish_development_in_bg refresh d)
-              in
-              ignore(clean ())));
+              let publish = locker (fun () ->
+                MatitamakeLib.publish_development_in_bg refresh d) in
+              ignore(publish ())));
+      connect_button develList#graphButton (fun () -> 
+        match get_devel_selected () with
+        | None -> ()
+        | Some d ->
+            (match MatitamakeLib.dot_for_development d with
+            | None -> ()
+            | Some _ ->
+                let browser = MatitaMathView.cicBrowser () in
+                browser#load (`Development
+                  (MatitamakeLib.name_for_development d))));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -634,35 +830,7 @@ class gui () =
         | MatitaScript.ActionCancelled s -> HLog.error s
         | exn ->
           if not (Helm_registry.get_bool "matita.debug") then
-           let floc, msg = MatitaExcPp.to_string exn in
-            begin
-             match floc with
-                None -> ()
-              | Some floc ->
-                 let (x, y) = HExtlib.loc_of_floc floc in
-                 let script = MatitaScript.current () in
-                 let locked_mark = script#locked_mark in
-                 let error_tag = script#error_tag in
-                 let baseoffset =
-                  (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
-                 let x' = baseoffset + x in
-                 let y' = baseoffset + y in
-                 let x_iter = source_buffer#get_iter (`OFFSET x') in
-                 let y_iter = source_buffer#get_iter (`OFFSET y') in
-                 source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
-                 let id = ref None in
-                 id := Some (source_buffer#connect#changed ~callback:(fun () ->
-                   source_buffer#remove_tag error_tag
-                     ~start:source_buffer#start_iter
-                     ~stop:source_buffer#end_iter;
-                   match !id with
-                   | None -> assert false (* a race condition occurred *)
-                   | Some id ->
-                       (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
-                 source_buffer#place_cursor
-                  (source_buffer#get_iter (`OFFSET x'));
-            end;
-            HLog.error msg
+           notify_exn exn
           else raise exn);
         (* script *)
       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
@@ -789,6 +957,7 @@ class gui () =
       connect_button main#scriptTopButton top;
       connect_button main#scriptBottomButton bottom;
       connect_button main#scriptJumpButton jump;
+      connect_button main#scriptAbortButton kill_worker;
       connect_menu_item main#scriptAdvanceMenuItem advance;
       connect_menu_item main#scriptRetractMenuItem retract;
       connect_menu_item main#scriptTopMenuItem top;
@@ -1007,16 +1176,34 @@ class gui () =
     method loadScript file =       
       let script = MatitaScript.current () in
       script#reset (); 
-      script#assignFileName file;
-      let content =
-       if Sys.file_exists file then file
-       else BuildTimeConf.script_template
-      in
-       source_view#source_buffer#begin_not_undoable_action ();
-       script#loadFromFile content;
-       source_view#source_buffer#end_not_undoable_action ();
-       console#message ("'"^file^"' loaded.");
-       self#_enableSaveTo file
+      if Pcre.pmatch ~pat:"\\.p$" file then
+        begin
+          let tptppath = 
+            Helm_registry.get_opt_default Helm_registry.string ~default:"./"
+              "matita.tptppath"
+          in
+          let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in
+          let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
+          script#assignFileName filename;
+          source_view#source_buffer#begin_not_undoable_action ();
+          script#loadFromString data;
+          source_view#source_buffer#end_not_undoable_action ();
+          console#message ("'"^filename^"' loaded.");
+          self#_enableSaveTo filename
+        end
+      else
+        begin
+          script#assignFileName file;
+          let content =
+           if Sys.file_exists file then file
+           else BuildTimeConf.script_template
+          in
+           source_view#source_buffer#begin_not_undoable_action ();
+           script#loadFromFile content;
+           source_view#source_buffer#end_not_undoable_action ();
+           console#message ("'"^file^"' loaded.");
+           self#_enableSaveTo file
+        end
       
     method setStar name b =
       let l = main#scriptLabel in
@@ -1055,11 +1242,6 @@ class gui () =
       dialog#check_widgets ();
       dialog
 
-    method newRecordDialog () =
-      let dialog = new recordChoiceDialog () in
-      dialog#check_widgets ();
-      dialog
-
     method newConfirmationDialog () =
       let dialog = new confirmationDialog () in
       dialog#check_widgets ();
@@ -1264,36 +1446,6 @@ class interpModel =
         tree_store#get ~row:iter ~column:interp_no_col
     end
 
-let interactive_interp_choice () = 
-  fun text prefix_len choices ->
-  let gui = instance () in
-  assert (choices <> []);
-  let dialog = gui#newRecordDialog () in
-  let model = new interpModel dialog#recordChoiceTreeView choices in
-  dialog#recordChoiceDialog#set_title "Interpretation choice";
-  dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
-  let interp_no = ref None in
-  let return _ =
-    dialog#recordChoiceDialog#destroy ();
-    GMain.Main.quit ()
-  in
-  let fail _ = interp_no := None; return () in
-  ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
-  connect_button dialog#recordChoiceOkButton (fun _ ->
-    match !interp_no with None -> () | Some _ -> return ());
-  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#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#recordChoiceDialog#show ();
-  GtkThread.main ();
-  (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
-
 let interactive_string_choice 
   text prefix_len ?(title = "") ?(msg = "") () ~id locs uris 
 =