Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
71b3c1ba
Commit
71b3c1ba
authored
Oct 29, 2010
by
MARCHE Claude
Browse files
gcd
parent
e4c65cc8
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/ide/gdbmain.ml
View file @
71b3c1ba
...
...
@@ -1089,62 +1089,83 @@ let (_ : GMenu.image_menu_item) =
~
callback
:
collapse_all_verified_things
()
let
rec
hide_proved_goal
g
=
let
rec
hide_proved_
in_
goal
g
=
if
g
.
Model
.
proved
then
begin
let
row
=
g
.
Model
.
goal_row
in
goals_view
#
collapse_row
(
goals
_model
#
get_path
row
);
goals_view
#
collapse_row
(
filter
_model
#
get_path
row
);
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
false
end
else
List
.
iter
(
fun
t
->
List
.
iter
hide_proved_goal
t
.
Model
.
subgoals
)
(
fun
t
->
List
.
iter
hide_proved_
in_
goal
t
.
Model
.
subgoals
)
g
.
Model
.
transformations
let
hide_verified_theories
()
=
List
.
iter
(
fun
th
->
if
th
.
Model
.
verified
then
begin
let
row
=
th
.
Model
.
theory_row
in
goals_view
#
collapse_row
(
goals_model
#
get_path
row
);
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
false
end
else
List
.
iter
hide_proved_goal
th
.
Model
.
goals
)
[]
(* !Model.all *)
let
hide_proved_in_theory
th
=
if
th
.
Model
.
verified
then
begin
let
row
=
th
.
Model
.
theory_row
in
goals_view
#
collapse_row
(
filter_model
#
get_path
row
);
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
false
end
else
List
.
iter
hide_proved_in_goal
th
.
Model
.
goals
let
hide_proved_in_file
f
=
if
f
.
Model
.
file_verified
then
begin
let
row
=
f
.
Model
.
file_row
in
goals_view
#
collapse_row
(
filter_model
#
get_path
row
);
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
false
end
else
List
.
iter
hide_proved_in_theory
f
.
Model
.
theories
let
hide_proved_in_files
()
=
List
.
iter
hide_proved_in_file
!
Model
.
all_files
let
rec
show_all_goal
s
g
=
let
rec
show_all_
in_
goal
g
=
let
row
=
g
.
Model
.
goal_row
in
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
true
;
if
g
.
Model
.
proved
then
goals_view
#
collapse_row
(
goals
_model
#
get_path
row
)
goals_view
#
collapse_row
(
filter
_model
#
get_path
row
)
else
goals_view
#
expand_row
(
goals
_model
#
get_path
row
);
goals_view
#
expand_row
(
filter
_model
#
get_path
row
);
List
.
iter
(
fun
t
->
List
.
iter
show_all_goal
s
t
.
Model
.
subgoals
)
(
fun
t
->
List
.
iter
show_all_
in_
goal
t
.
Model
.
subgoals
)
g
.
Model
.
transformations
let
show_all_theories
()
=
List
.
iter
(
fun
th
->
let
row
=
th
.
Model
.
theory_row
in
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
true
;
if
th
.
Model
.
verified
then
goals_view
#
collapse_row
(
goals_model
#
get_path
row
)
else
goals_view
#
expand_row
(
goals_model
#
get_path
row
);
List
.
iter
show_all_goals
th
.
Model
.
goals
)
[]
(* !Model.all *)
let
show_all_in_theory
th
=
let
row
=
th
.
Model
.
theory_row
in
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
true
;
if
th
.
Model
.
verified
then
goals_view
#
collapse_row
(
filter_model
#
get_path
row
)
else
begin
goals_view
#
expand_row
(
filter_model
#
get_path
row
);
List
.
iter
show_all_in_goal
th
.
Model
.
goals
end
let
show_all_in_file
f
=
let
row
=
f
.
Model
.
file_row
in
goals_model
#
set
~
row
~
column
:
Model
.
visible_column
true
;
if
f
.
Model
.
file_verified
then
goals_view
#
collapse_row
(
filter_model
#
get_path
row
)
else
begin
goals_view
#
expand_row
(
filter_model
#
get_path
row
);
List
.
iter
show_all_in_theory
f
.
Model
.
theories
end
let
show_all_in_files
()
=
List
.
iter
show_all_in_file
!
Model
.
all_files
let
(
_
:
GMenu
.
check_menu_item
)
=
view_factory
#
add_check_item
~
callback
:
(
fun
b
->
Model
.
toggle_hide_proved_goals
:=
b
;
if
b
then
hide_
verified_theori
es
()
else
show_all_
theori
es
()
)
if
b
then
hide_
proved_in_fil
es
()
else
show_all_
in_fil
es
()
)
"Hide proved goals"
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment