X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=b230adecc50f41ae68cb8c22c3facd47b25ac30d;hb=6f2481585178340b6f174f2db3323f4eb52282ef;hp=7decc583c58ab4b8de1b7a0dab4b49867792bae9;hpb=d90d73349df641ea2d18b4c2ff4fe9d970861778;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 7decc583c..b230adecc 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -70,47 +70,55 @@ let clean_current_baseuri grafite_status =
     with GrafiteTypes.Option_error _ -> ()
 
 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
-  let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname 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
-     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 
     
@@ -604,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;
@@ -890,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
@@ -933,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;
@@ -1255,7 +1264,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
@@ -1284,6 +1294,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 ());