Commit 3d629643 authored by MARCHE Claude's avatar MARCHE Claude

minor details

parent e5ba14eb
...@@ -672,8 +672,6 @@ let rec update_status_column_from_iter cont iter = ...@@ -672,8 +672,6 @@ let rec update_status_column_from_iter cont iter =
| Some p -> update_status_column_from_iter cont p | Some p -> update_status_column_from_iter cont p
| None -> () | None -> ()
let match_transformation_exception (e: exn) =
message_zone#buffer#set_text (Pp.sprintf "%a" Exn_printer.exn_printer e)
let move_current_row_selection_up () = let move_current_row_selection_up () =
let current_view = List.hd (goals_view#selection#get_selected_rows) in let current_view = List.hd (goals_view#selection#get_selected_rows) in
...@@ -707,7 +705,9 @@ let callback_update_tree_transform cont status = ...@@ -707,7 +705,9 @@ let callback_update_tree_transform cont status =
(* Put the selection on the first goal *) (* Put the selection on the first goal *)
goals_view#selection#select_iter (row_from_pn first_goal)#iter goals_view#selection#select_iter (row_from_pn first_goal)#iter
| [] -> ()) | [] -> ())
| TSfailed e -> match_transformation_exception e | TSfailed e ->
message_zone#buffer#set_text
(Pp.sprintf "%a" Exn_printer.exn_printer e)
| _ -> () | _ -> ()
let rec apply_transform cont t args = let rec apply_transform cont t args =
......
...@@ -97,7 +97,14 @@ let unproven_goals_in_session cont = ...@@ -97,7 +97,14 @@ let unproven_goals_in_session cont =
List.rev_append file_goals acc) List.rev_append file_goals acc)
files [] files []
let get_first_unproven_goal_around_pn_in_th cont pn = (*
[get_first_unproven_goal_around_pn_in_th cont pn]
returns the `first unproven goal' 'after' [pn]. Precisely:
(1) it finds the youngest ancestor a of [pn] that is not proved
(2) it returns the first unproved leaf of a
it returns None if all ancestors are proved (in the theory)
*)
let get_first_unproven_goal_around_pn_in_th cont pn : proofNodeID option =
let ses = cont.controller_session in let ses = cont.controller_session in
let rec look_around pn = let rec look_around pn =
match get_proof_parent ses pn with match get_proof_parent ses pn with
......
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