X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=f4024c3cbad5a72cece6c125a721184efe3e17fc;hb=69d232a6857da33782b1610aadfee41b9f5f09ef;hp=5bab5ab0ab4dcad44763fca84578cbe89c966ea8;hpb=b74ef6550e31214a340dfeae67ce77d055e9827c;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 5bab5ab0a..f4024c3cb 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -233,25 +233,30 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
   let errorll' =
    let remove_non_significant =
      List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
-   if all_passes then errorll else
+   let annotated_errorll () =
+    List.rev
+     (snd
+       (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[])
+         errorll)) in
+   if all_passes then annotated_errorll () else
      let safe_list_nth l n = try List.nth l n with Failure _ -> [] in
     (* We remove passes 1,2 and 5,6 *)
      let res =
-      []::[]
-      ::(remove_non_significant (safe_list_nth errorll 2))
-      ::(remove_non_significant (safe_list_nth errorll 3))
-      ::[]::[]
+      (1,[])::(2,[])
+      ::(3,remove_non_significant (safe_list_nth errorll 2))
+      ::(4,remove_non_significant (safe_list_nth errorll 3))
+      ::(5,[])::(6,[])::[]
      in
-      if List.flatten res <> [] then res
+      if List.flatten (List.map snd res) <> [] then res
       else
        (* all errors (if any) are not significant: we keep them *)
        let res =
-        []::[]
-        ::(safe_list_nth errorll 2)
-        ::(safe_list_nth errorll 3)
-        ::[]::[]
+        (1,[])::(2,[])
+        ::(3,(safe_list_nth errorll 2))
+        ::(4,(safe_list_nth errorll 3))
+        ::(5,[])::(6,[])::[]
        in
-        if List.flatten res <> [] then
+        if List.flatten (List.map snd res) <> [] then
 	 begin
           HLog.warn
 	   "All disambiguation errors are not significant. Showing them anyway." ;
@@ -261,18 +266,16 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
          begin
           HLog.warn
 	   "No errors in phases 2 and 3. Showing all errors in all phases" ;
-          errorll
+          annotated_errorll ()
          end
    in
   let choices =
-   let pass = ref 0 in
    List.flatten
     (List.map
-      (fun l ->
-        incr pass;
+      (fun (pass,l) ->
         List.map
          (fun (env,diff,offset,msg,significant) ->
-           offset, [[!pass], [[!pass], env, diff], msg, significant]) l
+           offset, [[pass], [[pass], env, diff], msg, significant]) 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
@@ -860,6 +863,7 @@ class gui () =
                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
               in
               ignore(clean ())));
+      (* publish button hidden, use command line 
       connect_button develList#publishButton 
         (locker (fun () -> 
           match get_devel_selected () with
@@ -868,6 +872,8 @@ class gui () =
               let publish = locker (fun () ->
                 MatitamakeLib.publish_development_in_bg refresh d) in
               ignore(publish ())));
+              *)
+      develList#publishButton#misc#hide ();
       connect_button develList#graphButton (fun () -> 
         match get_devel_selected () with
         | None -> ()
@@ -1144,10 +1150,13 @@ class gui () =
       self#updateFontSize ();
         (* debug menu *)
       main#debugMenu#misc#hide ();
-        (* status bar *)
+        (* HBUGS *)
+      main#hintNotebook#misc#hide ();
+      (*
       main#hintLowImage#set_file (image_path "matita-bulb-low.png");
       main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
       main#hintHighImage#set_file (image_path "matita-bulb-high.png");
+      *)
         (* focus *)
       self#sourceView#misc#grab_focus ();
         (* main win dimension *)
@@ -1379,11 +1388,13 @@ class gui () =
         end
       
     method setStar name b =
-      let l = main#scriptLabel in
+      let w = main#toplevel in
+      let set x = w#set_title x in
+      let name = "Matita - " ^ name in
       if b then
-        l#set_text (name ^  " *")
+        set (name ^  " *")
       else
-        l#set_text (name)
+        set (name)
         
     method private _enableSaveTo file =
       script_fname <- Some file;