Commit 47765f58 authored by Sylvain Dailler's avatar Sylvain Dailler

ide: Querying (print/search) on a proofAttempt = querying on its parent.

parent 778feeab
......@@ -366,6 +366,13 @@ type command =
| QError of string
| Other of string * string list
let query_on_task cont f id args =
let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
let interp commands_table cont id s =
let cmd,args = split_args s in
match Stdlib.Hstr.find commands_table cmd with
......@@ -374,11 +381,12 @@ let interp commands_table cont id s =
match f,id with
| Qnotask f, _ -> Query (f cont args)
| Qtask f, Some (Session_itp.APn id) ->
let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
in s
query_on_task cont f id args
| Qtask f, Some (Session_itp.APa pid) ->
let id = Session_itp.get_proof_attempt_parent
cont.Controller_itp.controller_session pid
in
query_on_task cont f id args
| Qtask _, _ -> QError "please select a goal first"
end
| exception Not_found ->
......
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