Commit 87b2b7a3 authored by François Bobot's avatar François Bobot
Browse files

gmain : split dont be stuck after pushing the button.

The callback is inside one thread the call to the gui
and db are protected inside a sync. Especially the fold
left which add each subgoal are each one inside a sync.

Problem you cant select split before all the proof are added.

Perhaps we can
1) add to the model in one thread.
2) acces to the db and the gui inside sync (one sync for each fold_left)
parent 1ffc8925
...@@ -991,15 +991,18 @@ let prover_on_selected_goals pr = ...@@ -991,15 +991,18 @@ let prover_on_selected_goals pr =
let split_goal g = let split_goal g =
if not g.Model.proved then if not g.Model.proved then
let callback subgoals = let callback subgoals =
ignore (Thread.create (fun subgoals ->
if List.length subgoals >= 2 then if List.length subgoals >= 2 then
let transf_id_split = Db.transf_from_name "split_goal" in let transf_id_split =
(GtkThread.sync Db.transf_from_name) "split_goal" in
let db_transf = let db_transf =
Db.add_transformation g.Model.goal_db transf_id_split (GtkThread.sync Db.add_transformation)
g.Model.goal_db transf_id_split
in in
let tr = Helpers.add_transformation_row g db_transf (* subgoals *) in let tr = (GtkThread.sync Helpers.add_transformation_row) g db_transf
(* subgoals *) in
let goal_name = g.Model.goal_name in let goal_name = g.Model.goal_name in
let goals,_ = List.fold_left let fold = (fun (acc,count) subtask ->
(fun (acc,count) subtask ->
let _id = (Task.task_goal subtask).Decl.pr_name in let _id = (Task.task_goal subtask).Decl.pr_name in
let subgoal_name = let subgoal_name =
goal_name ^ "." ^ (string_of_int count) goal_name ^ "." ^ (string_of_int count)
...@@ -1010,11 +1013,11 @@ let split_goal g = ...@@ -1010,11 +1013,11 @@ let split_goal g =
Helpers.add_goal_row (Model.Transf tr) subgoal_name subtask Helpers.add_goal_row (Model.Transf tr) subgoal_name subtask
subtask_db subtask_db
in in
(goal :: acc, count+1)) (goal :: acc, count+1)) in
([],1) subgoals let goals,_ = List.fold_left (GtkThread.sync fold) ([],1) subgoals
in in
tr.Model.subgoals <- List.rev goals; tr.Model.subgoals <- List.rev goals;
g.Model.transformations <- tr :: g.Model.transformations g.Model.transformations <- tr :: g.Model.transformations) subgoals)
in in
Scheduler.apply_transformation_l ~callback Scheduler.apply_transformation_l ~callback
split_transformation g.Model.task split_transformation g.Model.task
...@@ -1049,9 +1052,10 @@ let split_selected_goal_or_children row = ...@@ -1049,9 +1052,10 @@ let split_selected_goal_or_children row =
let split_selected_goals () = let split_selected_goals () =
List.iter ignore (Thread.create (fun () ->
split_selected_goal_or_children List.iter
goals_view#selection#get_selected_rows split_selected_goal_or_children
goals_view#selection#get_selected_rows) ())
(*****************************************************) (*****************************************************)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment