tree_store#clear ();
let idx1 = ref ~-1 in
List.iter
- (fun _,lll ->
+ (fun (_,lll) ->
incr idx1;
let loc_row =
if List.length choices = 1 then
Some loc_row) in
let idx2 = ref ~-1 in
List.iter
- (fun passes,envs_and_diffs,_,_ ->
+ (fun (passes,envs_and_diffs,_,_) ->
incr idx2;
let msg_row =
if List.length lll = 1 then
String.concat "\n"
("" ::
List.map
- (fun k,desc ->
+ (fun (k,desc) ->
let alias =
match k with
| DisambiguateTypes.Id id ->
let source_view = (s ())#source_view in
main#buttonsToolbar#misc#set_sensitive true;
main#scriptMenu#misc#set_sensitive true;
- source_view#set_editable true;
- (*The next line seems sufficient to avoid some unknown race condition *)
- GtkThread.sync (fun () -> ()) ()
+ source_view#set_editable true
in
let worker_thread = ref None in
let notify_exn (source_view : GSourceView3.source_view) exn =
"apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
- let module Hr = Helm_registry in
MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
~callback:(function
| true -> main#toplevel#fullscreen ()