X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=b1b2a6ad3fa683c2856a9f4226bd547077534365;hb=ac8bbbb47941fdf5b2d602b1e2ab2a6d6dcec9cd;hp=34406a3cd147908ef96d76a9804ecafc3064815f;hpb=d39571d4fed32b6db8c355189bb099e2837eaf9c;p=helm.git
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 34406a3cd..b1b2a6ad3 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/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.\nShould I generate it?"
- (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.\nShould I generate it?"
+ (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
@@ -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;
@@ -1240,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
@@ -1269,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 ^ "" ^ str2 ^ "" ^ 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 ());