Commit 705831e5 authored by MARCHE Claude's avatar MARCHE Claude

apply_transf done by the why thread instead of the gui thread

parent d1f40640
......@@ -213,7 +213,6 @@ let () =
let split_transformation = Trans.lookup_transform_l "split_goal" env
module Ide_goals = struct
let cols = new GTree.column_list
......@@ -460,21 +459,23 @@ let split_unproved_goals ~(model:GTree.tree_store) ~(view:GTree.view) () =
let proved = model#get ~row ~column:Ide_goals.proved_column in
if not proved then
let goal_name = model#get ~row ~column:Ide_goals.name_column in
let split = Trans.apply split_transformation g in
if List.length split >= 2 then
let _ = List.fold_right
(fun subtask count ->
let id = (Task.task_goal subtask).Decl.pr_name in
let subtask_row = model#append ~parent:row () in
Ident.Hid.add Ide_goals.goal_table id (subtask,subtask_row);
model#set ~row:subtask_row ~column:Ide_goals.id_column id;
model#set ~row:subtask_row ~column:Ide_goals.visible_column true;
model#set ~row:subtask_row ~column:Ide_goals.name_column
(goal_name ^ "." ^ (string_of_int count));
count+1)
split 1
in
view#expand_row (model#get_path row)
let callback subgoals =
if List.length subgoals >= 2 then
let _ = List.fold_right
(fun subtask count ->
let id = (Task.task_goal subtask).Decl.pr_name in
let subtask_row = model#append ~parent:row () in
Ident.Hid.add Ide_goals.goal_table id (subtask,subtask_row);
model#set ~row:subtask_row ~column:Ide_goals.id_column id;
model#set ~row:subtask_row ~column:Ide_goals.visible_column true;
model#set ~row:subtask_row ~column:Ide_goals.name_column
(goal_name ^ "." ^ (string_of_int count));
count+1)
subgoals 1
in
view#expand_row (model#get_path row)
in
Scheduler.apply_transformation ~callback split_transformation g
)
Ide_goals.goal_table
......
......@@ -25,7 +25,9 @@ type attempt = bool * int * int * string * string * Driver.driver *
let prover_attempts_queue : attempt Queue.t = Queue.create ()
(* queue of transformations *)
let transf_queue : int Queue.t = Queue.create ()
let transf_queue :
((Task.task list -> unit) * 'a Trans.trans * Task.task) Queue.t
= Queue.create ()
(* queue of prover answers *)
let answers_queue : (attempt * proof_attempt_status * float) Queue.t
......@@ -65,11 +67,12 @@ let event_handler () =
!async (fun () -> callback res time) ()
with Queue.Empty ->
try
let _t = Queue.pop transf_queue in
let (callback,transf,task) = Queue.pop transf_queue in
Mutex.unlock queue_lock;
eprintf "[Why thread] Scheduler.event_handler: transformations not supported yet@.";
let subtasks : Task.task list = Trans.apply transf task in
(* TODO: update database *)
(* TODO: call GUI back given new subgoals *)
(* call GUI back given new subgoals *)
!async (fun () -> callback subtasks) ()
with Queue.Empty ->
(* since answers_queue and transf_queue are empty,
we are sure that both
......@@ -152,5 +155,12 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ~prover
Condition.signal queue_condition;
Mutex.unlock queue_lock;
()
let apply_transformation ~callback transf goal =
Mutex.lock queue_lock;
Queue.push (callback,transf,goal) transf_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock;
()
......@@ -66,6 +66,11 @@ val schedule_proof_attempt :
*)
val apply_transformation :
callback:(Why.Task.task list -> unit) ->
Why.Task.task list Trans.trans -> Task.task -> unit
(*
......
Markdown is supported
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