Commit 83e43450 authored by MARCHE Claude's avatar MARCHE Claude

do_intros is not an argument of get_task anymore

parent cee208dc
......@@ -790,7 +790,7 @@ end
let session = d.cont.Controller_itp.controller_session in
(match node with
| APn pr_node ->
let task,_table = Session_itp.get_task ~do_intros:false session pr_node in
let task = Session_itp.get_raw_task session pr_node in
let b = label_detection task in
if b then
(focused_node := Focus_on node;
......@@ -902,7 +902,13 @@ end
(* -- send the task -- *)
let task_of_id d id do_intros loc =
let task,tables = get_task ~do_intros d.cont.controller_session id in
let task,tables =
if do_intros then get_task d.cont.controller_session id
else
let task = get_raw_task d.cont.controller_session id in
let tables = Args_wrapper.build_naming_tables task in
task,tables
in
(* This function also send source locations associated to the task *)
let loc_color_list = if loc then get_locations task else [] in
let task_text =
......
......@@ -108,7 +108,7 @@ type session = {
session_prover_ids : int Hprover.t;
(* tasks *)
session_raw_tasks : Task.task Hpn.t;
session_tasks : (bool * Task.task * Trans.naming_table) Hpn.t;
session_tasks : (Task.task * Trans.naming_table) Hpn.t;
(* proved status *)
file_state: bool Hstr.t;
th_state: bool Ident.Hid.t;
......@@ -214,24 +214,14 @@ let get_proofNode (s : session) (id : proofNodeID) =
let get_raw_task s id =
Hpn.find s.session_raw_tasks id
let get_task ?do_intros s n =
let get_task s n =
try
let (b,ti,ta) = Hpn.find s.session_tasks n in
match do_intros with
| None -> (ti,ta)
| Some b' -> if b <> b' then raise Not_found; (ti,ta)
Hpn.find s.session_tasks n
with Not_found ->
let t = get_raw_task s n in
let do_intros =
match do_intros with
| None -> true
| Some b -> b
in
let ti =
if do_intros then Trans.apply Introduction.introduce_premises t else t
in
let ti = Trans.apply Introduction.introduce_premises t in
let ta = Args_wrapper.build_naming_tables ti in
Hpn.add s.session_tasks n (do_intros,ti,ta);
Hpn.add s.session_tasks n (ti,ta);
ti,ta
let get_transfNode (s : session) (id : transID) =
......
......@@ -84,8 +84,9 @@ val is_below: session -> any -> any -> bool
type proof_parent = Trans of transID | Theory of theory
val get_raw_task : session -> proofNodeID -> Task.task
val get_task : ?do_intros:bool -> session -> proofNodeID -> Task.task * Trans.naming_table
val get_task : session -> proofNodeID -> Task.task * Trans.naming_table
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
......
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