open MatitaGtkMisc
open MatitaMisc
-exception Found of int
-
let all_disambiguation_passes = ref false
(* this is a shit and should be changed :-{ *)
?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
?copy_cb ()
- ~id uris
+ ~id:_ uris
=
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
| uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
+ (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling
+ other dialogs *)
GtkThread.main ();
(match !choices with
| None -> raise MatitaTypes.Cancel
(let loc_row = tree_store#append () in
begin
match lll with
- [passes,envs_and_diffs,_,_] ->
+ [passes,_envs_and_diffs,_,_] ->
tree_store#set ~row:loc_row ~column:id_col
("Error location " ^ string_of_int (!idx1+1) ^
", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
+ GtkThread.sync (fun _ ->
let dialog = new disambiguationErrors () in
- if all_passes then
- dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+ dialog#toplevel#add_button "Fix this interpretation" `OK;
+ dialog#toplevel#add_button "Close" `DELETE_EVENT;
+ if not all_passes then
+ dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
let model = new interpErrorModel dialog#treeview choices in
dialog#disambiguationErrors#set_title "Disambiguation error";
dialog#disambiguationErrorsLabel#set_label
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
));
- let return _ =
- dialog#disambiguationErrors#destroy ();
- GMain.Main.quit ()
+ (match GtkThread.sync dialog#toplevel#run () with
+ | `OK ->
+ let tree_path =
+ match fst (dialog#treeview#get_cursor ()) with
+ None -> assert false
+ | Some tp -> tp in
+ let idx1,idx2,idx3 = model#get_interp_no tree_path in
+ let diff =
+ match idx2,idx3 with
+ Some idx2, Some idx3 ->
+ let _,lll = List.nth choices idx1 in
+ let _,envs_and_diffs,_,_ = List.nth lll idx2 in
+ let _,_,diff = List.nth envs_and_diffs idx3 in
+ diff
+ | _,_ -> assert false
in
- let fail _ = return () in
- ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
- connect_button dialog#disambiguationErrorsOkButton
- (fun _ ->
- let tree_path =
- match fst (dialog#treeview#get_cursor ()) with
- None -> assert false
- | Some tp -> tp in
- let idx1,idx2,idx3 = model#get_interp_no tree_path in
- let diff =
- match idx2,idx3 with
- Some idx2, Some idx3 ->
- let _,lll = List.nth choices idx1 in
- let _,envs_and_diffs,_,_ = List.nth lll idx2 in
- let _,_,diff = List.nth envs_and_diffs idx3 in
- diff
- | _,_ -> assert false
- in
- let newtxt =
- String.concat "\n"
- ("" ::
- List.map
- (fun k,desc ->
- let alias =
- match k with
- | DisambiguateTypes.Id id ->
- GrafiteAst.Ident_alias (id, desc)
- | DisambiguateTypes.Symbol (symb, i)->
- GrafiteAst.Symbol_alias (symb, i, desc)
- | DisambiguateTypes.Num i ->
- GrafiteAst.Number_alias (i, desc)
- in
- GrafiteAstPp.pp_alias alias)
- diff) ^ "\n"
- in
- source_buffer#insert
- ~iter:
- (source_buffer#get_iter_at_mark
- (`NAME "beginning_of_statement")) newtxt ;
- return ()
- );
- connect_button dialog#disambiguationErrorsMoreErrors
- (fun _ -> return () ; raise UseLibrary);
- connect_button dialog#disambiguationErrorsCancelButton fail;
- dialog#disambiguationErrors#show ();
- GtkThread.main ()
-
+ let newtxt =
+ String.concat "\n"
+ ("" ::
+ List.map
+ (fun k,desc ->
+ let alias =
+ match k with
+ | DisambiguateTypes.Id id ->
+ GrafiteAst.Ident_alias (id, desc)
+ | DisambiguateTypes.Symbol (symb, i)->
+ GrafiteAst.Symbol_alias (symb, i, desc)
+ | DisambiguateTypes.Num i ->
+ GrafiteAst.Number_alias (i, desc)
+ in
+ GrafiteAstPp.pp_alias alias)
+ diff) ^ "\n"
+ in
+ source_buffer#insert
+ ~iter:
+ (source_buffer#get_iter_at_mark
+ (`NAME "beginning_of_statement")) newtxt
+ | `HELP (* HELP MEANS MORE *) ->
+ dialog#toplevel#destroy () ;
+ raise UseLibrary
+ | `DELETE_EVENT -> ()
+ | _ -> assert false) ;
+ dialog#toplevel#destroy ()
+ ) ()
class gui () =
(* creation order _is_ relevant for windows placement *)
let saved_use_library= !MultiPassDisambiguator.use_library in
try
MultiPassDisambiguator.use_library := !all_disambiguation_passes;
+ prerr_endline "PRIMA";
f script;
MultiPassDisambiguator.use_library := saved_use_library;
- unlock_world ()
+ prerr_endline "DOPO";
+ unlock_world () ;
+ prerr_endline "FINE";
with
| MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+ prerr_endline "EXC1";
(try
interactive_error_interp
~all_passes:!all_disambiguation_passes source_view#source_buffer
notify_exn source_view exc);
| exc -> notify_exn source_view exc);
MultiPassDisambiguator.use_library := saved_use_library;
- unlock_world ()
+ prerr_endline "DOPO1";
+ unlock_world ();
+ prerr_endline "FINE1"
| exc ->
(try notify_exn source_view exc
with Sys.Break as e -> notify_exn source_view e);
save_moo script#status;
true
| `NO -> true
- | `CANCEL -> false
+ | `DELETE_EVENT -> false
else
(save_moo script#status; true)
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
- method private _enableSaveTo file =
+ method private _enableSaveTo _file =
self#main#saveMenuItem#misc#set_sensitive true
method private console = console
let interactive_string_choice
- text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
+ text prefix_len ?(title = "") ?msg:(_ = "") () ~id:_ locs uris
=
+ GtkThread.sync (fun _ ->
let dialog = new uriChoiceDialog () in
dialog#uriEntryHBox#misc#hide ();
dialog#uriChoiceSelectedButton#misc#hide ();
dialog#uriChoiceTreeView#selection#set_mode
(`SINGLE :> Gtk.Tags.selection_mode);
let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
+ let choices = ref [] in
dialog#uriChoiceDialog#set_title title;
let hack_len = MatitaGtkMisc.utf8_string_length text in
let rec colorize acc_len = function
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);
+ | uris -> choices := uris; dialog#toplevel#response `OK);
+ connect_button dialog#uriChoiceAbortButton (fun _ -> dialog#toplevel#response `DELETE_EVENT);
dialog#uriChoiceDialog#show ();
- GtkThread.main ();
- (match !choices with
- | None -> raise MatitaTypes.Cancel
- | Some uris -> uris)
+ let res =
+ match dialog#toplevel#run () with
+ | `DELETE_EVENT -> dialog#toplevel#destroy() ; raise MatitaTypes.Cancel
+ | `OK -> !choices
+ | _ -> assert false in
+ dialog#toplevel#destroy () ;
+ res) ()
let interactive_interp_choice () text prefix_len choices =
(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
let _ =
(* disambiguator callbacks *)
Disambiguate.set_choose_uris_callback
- (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
+ (fun ~selection_mode ?ok ?enable_button_for_non_vars:(_=false) ~title ~msg ->
interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
(* gtk initialization *)
projects / helm.git / blobdiff