X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=7270603a9636b7ebcd4be445ce9350b0757dfefb;hb=8030b740ba0b84df1ae3a3e5878b447f3e4ec874;hp=ed739eefbebb8c9be4a9e5ab95f919166625a722;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ed739eefb..7270603a9 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -66,50 +66,59 @@ class console ~(buffer: GText.buffer) () =
 let clean_current_baseuri grafite_status = 
     try  
       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
-      let basedir = Helm_registry.get "matita.basedir" in
-      LibraryClean.clean_baseuris ~basedir [baseuri]
+      LibraryClean.clean_baseuris [baseuri]
     with GrafiteTypes.Option_error _ -> ()
 
 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
-  let basedir = Helm_registry.get "matita.basedir" in
-  let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
-  let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
-  let save () =
-    let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
-    let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri
-    in
-     GrafiteMarshal.save_moo moo_fname
-      grafite_status.GrafiteTypes.moo_content_rev;
-     LibraryNoDb.save_metadata metadata_fname
-      lexicon_status.LexiconEngine.metadata;
-     LexiconMarshal.save_lexicon lexicon_fname
-      lexicon_status.LexiconEngine.lexicon_content_rev
+  let baseuri =
+   try Some (GrafiteTypes.get_string_option grafite_status "baseuri")
+   with GrafiteTypes.Option_error _ -> None
   in
   if (MatitaScript.current ())#eos &&
-     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+     grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof &&
+     baseuri <> None
   then
-    begin
-      let rc = 
-        MatitaGtkMisc.ask_confirmation
-        ~title:"A .moo can be generated"
-        ~message:(Printf.sprintf 
-          "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          (Filename.basename moo_fname) (Filename.basename fname))
-        ~parent ()
-      in
-      let b = 
-        match rc with 
-        | `YES -> true 
-        | `NO -> false 
-        | `CANCEL -> raise MatitaTypes.Cancel 
+   begin
+    let baseuri = match baseuri with Some b -> b | None -> assert false in
+    let moo_fname = 
+     LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
+      ~writable:true in
+    let save () =
+      let metadata_fname =
+       LibraryMisc.metadata_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true in
+      let lexicon_fname =
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true
       in
-      if b then
-          save ()
-      else
-        clean_current_baseuri grafite_status
-    end
+       GrafiteMarshal.save_moo moo_fname
+        grafite_status.GrafiteTypes.moo_content_rev;
+       LibraryNoDb.save_metadata metadata_fname
+        lexicon_status.LexiconEngine.metadata;
+       LexiconMarshal.save_lexicon lexicon_fname
+        lexicon_status.LexiconEngine.lexicon_content_rev
+    in
+     begin
+       let rc = 
+         MatitaGtkMisc.ask_confirmation
+         ~title:"A .moo can be generated"
+         ~message:(Printf.sprintf 
+           "%s can be generated for %s.\n<i>Should I generate it?</i>"
+           (Filename.basename moo_fname) (Filename.basename fname))
+         ~parent ()
+       in
+       let b = 
+         match rc with 
+         | `YES -> true 
+         | `NO -> false 
+         | `CANCEL -> raise MatitaTypes.Cancel 
+       in
+       if b then
+           save ()
+       else
+         clean_current_baseuri grafite_status
+     end
+   end
   else
     clean_current_baseuri grafite_status 
     
@@ -206,6 +215,11 @@ class gui () =
         ~website:"http://helm.cs.unibo.it"
         ()
       in
+      connect_menu_item main#contentsMenuItem (fun () ->
+        let cmd =
+          sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir
+        in
+        ignore (Sys.command cmd));
       connect_menu_item main#aboutMenuItem about_dialog#present;
         (* findRepl win *)
       let show_find_Repl () = 
@@ -467,6 +481,15 @@ class gui () =
                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
               in
               ignore(clean ())));
+      connect_button develList#publishButton 
+        (locker (fun () -> 
+          match get_devel_selected () with
+          | None -> ()
+          | Some d -> 
+              let clean = locker 
+                (fun () -> MatitamakeLib.publish_development_in_bg refresh d)
+              in
+              ignore(clean ())));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -589,7 +612,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,[])));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:main#tacticsBarMenuItem;
@@ -608,7 +631,7 @@ class gui () =
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
         (function 
-        | MatitaScript.ActionCancelled -> () 
+        | MatitaScript.ActionCancelled s -> HLog.error s
         | exn ->
           if not (Helm_registry.get_bool "matita.debug") then
            let floc, msg = MatitaExcPp.to_string exn in
@@ -875,6 +898,7 @@ class gui () =
     method private nextLigature () =
       let iter = source_buffer#get_iter_at_mark `INSERT in
       let write_ligature len s =
+        assert(Glib.Utf8.validate s);
         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
       in
@@ -918,7 +942,7 @@ class gui () =
           (match CicNotationLexer.lookup_ligatures ligature with
           | [] -> ()
           | hd :: tl ->
-              write_ligature (String.length ligature) hd;
+              write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd;
               next_ligatures <- tl @ [ hd ])
       | hd :: tl ->
           write_ligature 1 hd;
@@ -983,16 +1007,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
@@ -1133,7 +1175,7 @@ let interactive_uri_choice
   let gui = instance () in
   let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
   if (selection_mode <> `SINGLE) &&
-    (Helm_registry.get_bool "matita.auto_disambiguation")
+    (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
   then
     Lazy.force nonvars_uris
   else begin
@@ -1240,7 +1282,8 @@ class interpModel =
         tree_store#get ~row:iter ~column:interp_no_col
     end
 
-let interactive_interp_choice () choices =
+let interactive_interp_choice () = 
+  fun text prefix_len choices ->
   let gui = instance () in
   assert (choices <> []);
   let dialog = gui#newRecordDialog () in
@@ -1269,6 +1312,127 @@ let interactive_interp_choice () choices =
   GtkThread.main ();
   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
 
+let interactive_string_choice 
+  text prefix_len ?(title = "") ?(msg = "") () ~id locs uris 
+=
+  let gui = instance () in
+    let dialog = gui#newUriDialog () in
+    dialog#uriEntryHBox#misc#hide ();
+    dialog#uriChoiceSelectedButton#misc#hide ();
+    dialog#uriChoiceAutoButton#misc#hide ();
+    dialog#uriChoiceConstantsButton#misc#hide ();
+    dialog#uriChoiceTreeView#selection#set_mode
+      (`SINGLE :> Gtk.Tags.selection_mode);
+    let model = new stringListModel dialog#uriChoiceTreeView in
+    let choices = ref None in
+    dialog#uriChoiceDialog#set_title title; 
+    let hack_len = MatitaGtkMisc.utf8_string_length text in
+    let rec colorize acc_len = function
+      | [] -> 
+          let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
+          fst(MatitaGtkMisc.utf8_parsed_text text floc)
+      | he::tl -> 
+          let start, stop =  HExtlib.loc_of_floc he in
+          let floc1 = HExtlib.floc_of_loc (acc_len,start) in
+          let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
+          let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
+          str1 ^ "<b>" ^ str2 ^ "</b>" ^ colorize stop tl
+    in
+(*     List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
+                Printf.eprintf "(%d,%d)" start stop) locs; *)
+    let locs = 
+      List.sort 
+        (fun loc1 loc2 -> 
+          fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) 
+        locs 
+    in
+(*     prerr_endline "XXXXXXXXXXXXXXXXXXXX";
+    List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
+                Printf.eprintf "(%d,%d)" start stop) locs;
+    prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
+    dialog#uriChoiceLabel#set_use_markup true;
+    let txt = colorize 0 locs in
+    let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
+      (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
+    in
+    dialog#uriChoiceLabel#set_label txt;
+    List.iter model#easy_append uris;
+    let return v =
+      choices := v;
+      dialog#uriChoiceDialog#destroy ();
+      GMain.Main.quit ()
+    in
+    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+    connect_button dialog#uriChoiceForwardButton (fun _ ->
+      match model#easy_selection () with
+      | [] -> ()
+      | uris -> return (Some uris));
+    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+    dialog#uriChoiceDialog#show ();
+    GtkThread.main ();
+    (match !choices with 
+    | None -> raise MatitaTypes.Cancel
+    | Some uris -> uris)
+
+let interactive_interp_choice () text prefix_len choices =
+(*  List.iter (fun (l,_,_) -> 
+   List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
+   Printf.eprintf "(%d,%d)" start stop) l; prerr_endline "")
+   ((List.hd choices)); *)
+ let filter_choices filter =
+  let rec is_compatible filter =
+   function
+      [] -> true
+    | (_,id,dsc)::tl ->
+       try
+        if List.assoc id filter = dsc then
+         is_compatible filter tl
+        else
+         false
+       with
+        Not_found -> true
+  in
+   List.filter (fun (_,interp) -> is_compatible filter interp)
+ in
+ let rec get_choices id =
+  function
+     [] -> []
+   | (_,he)::tl ->
+      let _,_,dsc = List.find (fun (_,id',_) -> id = id') he in
+       dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices id tl))
+ in
+ let example_interp =
+  match choices with
+     [] -> assert false
+   | he::_ -> he in
+ let ask_user id locs choices =
+  interactive_string_choice
+   text prefix_len
+   ~title:"Ambiguous input"
+   ~msg:("Choose an interpretation for " ^ id) () ~id locs choices
+ in
+ let rec classify ids filter partial_interpretations =
+  match ids with
+     [] -> List.map fst partial_interpretations
+   | (locs,id,_)::tl ->
+      let choices = get_choices id partial_interpretations in
+      let chosen_dsc =
+       match choices with
+          [dsc] -> dsc
+        | _ ->
+          match ask_user id locs choices with
+             [x] -> x
+           | _ -> assert false
+      in
+      let filter = (id,chosen_dsc)::filter in
+      let compatible_interps = filter_choices filter partial_interpretations in
+       classify tl filter compatible_interps in
+ let enumerated_choices =
+  let idx = ref ~-1 in
+  List.map (fun interp -> incr idx; !idx,interp) choices
+ in
+  classify example_interp [] enumerated_choices
+
 let _ =
   (* disambiguator callbacks *)
   GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());