Commit 02876411 authored by MARCHE Claude's avatar MARCHE Claude

use of GTree row_reference in new interface

parent 4faeadaf
......@@ -41,9 +41,9 @@ module Array
parameter length : a:array 'a -> {} int reads a { result = length a }
parameter make : n:int -> v:'a ->
{}
array 'a
parameter make : n:int -> v:'a ->
{}
array 'a
{ length result = n and forall i:int. 0 <= i < n -> result[i] = v}
parameter append : a1:array 'a -> a2:array 'a ->
......@@ -59,38 +59,38 @@ module Array
{ length result = len and
forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
parameter copy : a:array 'a ->
{}
array 'a
{ length result = length a and
parameter copy : a:array 'a ->
{}
array 'a
{ length result = length a and
forall i:int. 0 <= i < length result -> result[i] = a[i] }
parameter fill : a:array 'a -> ofs:int -> len:int -> v:'a ->
{ 0 <= ofs and ofs + len <= length a }
unit
writes a
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
(forall i:int.
ofs <= i < ofs + len -> a[i] = v) }
parameter blit :
parameter blit :
a1:array 'a -> ofs1:int -> a2:array 'a -> ofs2:int -> len:int ->
{ 0 <= ofs1 and ofs1 + len <= length a1 and
0 <= ofs2 and ofs2 + len <= length a2 }
unit
writes a2
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
(* TODO?
- concat : 'a array list -> 'a array
- to_list
- of_list
- of_list
*)
end
......@@ -131,7 +131,7 @@ module TestArray
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C .. modules/stdlib"
End:
End:
*)
......@@ -359,12 +359,19 @@ let image_of_result ~obsolete result =
module M = Session.Make
(struct
type key = Gtk.tree_iter
type key = GTree.row_reference
let create ?parent () =
let parent = match parent with
| None -> None
| Some r -> Some r#iter
in
let iter = goals_model#append ?parent () in
goals_model#get_row_reference (goals_model#get_path iter)
let create ?parent () = goals_model#append ?parent ()
let remove row =
let (_:bool) = goals_model#remove row in ()
let (_:bool) = goals_model#remove row#iter in ()
let idle f =
let (_ : GMain.Idle.id) = GMain.Idle.add f in ()
......@@ -378,18 +385,18 @@ module M = Session.Make
let set_row_status row b =
if b then
begin
goals_view#collapse_row (goals_model#get_path row);
goals_model#set ~row ~column:status_column !image_yes;
goals_view#collapse_row row#path;
goals_model#set ~row:row#iter ~column:status_column !image_yes;
end
else
begin
goals_model#set ~row ~column:status_column !image_unknown;
goals_model#set ~row:row#iter ~column:status_column !image_unknown;
end
let set_proof_state ~obsolete a =
let row = a.M.proof_key in
let res = a.M.proof_state in
goals_model#set ~row ~column:status_column
goals_model#set ~row:row#iter ~column:status_column
(image_of_result ~obsolete res);
let t = match res with
| Session.Done { Call_provers.pr_time = time } ->
......@@ -397,7 +404,7 @@ let set_proof_state ~obsolete a =
| _ -> ""
in
let t = if obsolete then t ^ " (obsolete)" else t in
goals_model#set ~row ~column:time_column t
goals_model#set ~row:row#iter ~column:time_column t
let model_index = Hashtbl.create 17
......@@ -413,15 +420,15 @@ let init =
fun row any ->
incr cpt;
Hashtbl.add model_index !cpt any;
goals_model#set ~row ~column:index_column !cpt;
goals_model#set ~row ~column:icon_column
goals_model#set ~row:row#iter ~column:index_column !cpt;
goals_model#set ~row:row#iter ~column:icon_column
(match any with
| M.Goal _ -> !image_file
| M.Theory _
| M.File _ -> !image_directory
| M.Proof_attempt _ -> !image_prover
| M.Transformation _ -> !image_transf);
goals_model#set ~row ~column:name_column
goals_model#set ~row:row#iter ~column:name_column
(match any with
| M.Goal g -> M.goal_expl g
| M.Theory th -> M.theory_name th
......@@ -711,7 +718,7 @@ let rec collapse_proved_goal g =
if M.goal_proved g then
begin
let row = M.goal_key g in
goals_view#collapse_row (goals_model#get_path row);
goals_view#collapse_row row#path;
end
else
Hashtbl.iter
......@@ -722,7 +729,7 @@ let collapse_verified_theory th =
if M.verified th then
begin
let row = M.theory_key th in
goals_view#collapse_row (goals_model#get_path row);
goals_view#collapse_row row#path;
end
else
List.iter collapse_proved_goal (M.goals th)
......@@ -731,7 +738,7 @@ let collapse_verified_file f =
if f.M.file_verified then
begin
let row = f.M.file_key in
goals_view#collapse_row (goals_model#get_path row);
goals_view#collapse_row row#path;
end
else
List.iter collapse_verified_theory f.M.theories
......
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