Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
687ab81e
Commit
687ab81e
authored
Mar 30, 2011
by
MARCHE Claude
Browse files
prover_data moved to module Session
parent
9604ca5f
Changes
6
Hide whitespace changes
Inline
Side-by-side
src/ide/gconfig.ml
View file @
687ab81e
...
...
@@ -24,7 +24,8 @@ open Rc
open
Whyconf
type
prover_data
=
type
prover_data
=
Session
.
prover_data
(*
{ prover_id : string;
prover_name : string;
prover_version : string;
...
...
@@ -33,6 +34,7 @@ type prover_data =
driver : Driver.driver;
mutable editor : string;
}
*)
type
t
=
{
mutable
window_width
:
int
;
...
...
@@ -85,24 +87,6 @@ let load_ide section =
"default_editor"
;
}
let
get_prover_data
env
id
pr
acc
=
try
let
dr
=
Driver
.
load_driver
env
pr
.
Whyconf
.
driver
in
Mstr
.
add
id
{
prover_id
=
id
;
prover_name
=
pr
.
Whyconf
.
name
;
prover_version
=
pr
.
Whyconf
.
version
;
command
=
pr
.
Whyconf
.
command
;
driver_name
=
pr
.
Whyconf
.
driver
;
driver
=
dr
;
editor
=
pr
.
Whyconf
.
editor
;
}
acc
with
_e
->
eprintf
"Failed to load driver %s for prover %s. prover disabled@."
pr
.
Whyconf
.
driver
pr
.
Whyconf
.
name
;
acc
let
load_config
config
=
let
main
=
get_main
config
in
let
ide
=
match
get_section
config
"ide"
with
...
...
@@ -144,13 +128,13 @@ let read_config () =
let
save_config
t
=
let
save_prover
_
pr
acc
=
Mstr
.
add
pr
.
prover_id
Mstr
.
add
pr
.
Session
.
prover_id
{
Whyconf
.
name
=
pr
.
prover_name
;
command
=
pr
.
command
;
driver
=
pr
.
driver_name
;
version
=
pr
.
prover_version
;
editor
=
pr
.
editor
;
Whyconf
.
name
=
pr
.
Session
.
prover_name
;
command
=
pr
.
Session
.
command
;
driver
=
pr
.
Session
.
driver_name
;
version
=
pr
.
Session
.
prover_version
;
editor
=
pr
.
Session
.
editor
;
}
acc
in
let
config
=
t
.
config
in
let
config
=
set_main
config
...
...
@@ -420,7 +404,7 @@ let run_auto_detection gconfig =
let
config
=
Autodetection
.
run_auto_detection
gconfig
.
config
in
gconfig
.
config
<-
config
;
let
provers
=
get_provers
config
in
gconfig
.
provers
<-
Mstr
.
fold
(
get_prover_data
gconfig
.
env
)
provers
Mstr
.
empty
gconfig
.
provers
<-
Mstr
.
fold
(
Session
.
get_prover_data
gconfig
.
env
)
provers
Mstr
.
empty
let
()
=
eprintf
"end of configuration initialization@."
...
...
src/ide/gconfig.mli
View file @
687ab81e
...
...
@@ -19,7 +19,8 @@
open
Why
type
prover_data
=
type
prover_data
=
Session
.
prover_data
(*
{ prover_id : string;
prover_name : string;
prover_version : string;
...
...
@@ -28,6 +29,7 @@ type prover_data =
driver : Driver.driver;
mutable editor : string;
}
*)
type
t
=
{
mutable
window_width
:
int
;
...
...
@@ -45,9 +47,11 @@ type t =
mutable
config
:
Whyconf
.
config
;
}
(*
val get_prover_data : Why.Env.env -> string ->
Why.Whyconf.config_prover ->
prover_data Why.Util.Mstr.t -> prover_data Why.Util.Mstr.t
*)
val
save_config
:
unit
->
unit
...
...
@@ -97,6 +101,6 @@ val run_auto_detection : t -> unit
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/whyide.
opt
"
compile-command: "unset LANG; make -C ../.. bin/why
3
ide.
byte
"
End:
*)
src/ide/gmain.ml
View file @
687ab81e
...
...
@@ -151,7 +151,7 @@ let gconfig =
c
.
env
<-
Lexer
.
create_env
loadpath
;
let
provers
=
Whyconf
.
get_provers
c
.
Gconfig
.
config
in
c
.
provers
<-
Util
.
Mstr
.
fold
(
Gconfig
.
get_prover_data
c
.
env
)
provers
Util
.
Mstr
.
empty
;
Util
.
Mstr
.
fold
(
Session
.
get_prover_data
c
.
env
)
provers
Util
.
Mstr
.
empty
;
c
let
()
=
...
...
@@ -917,11 +917,11 @@ module Helpers = struct
let
add_external_proof_row
~
obsolete
~
edit
g
p
db_proof
result
(*_time*)
=
let
parent
=
g
.
goal_row
in
let
name
=
p
.
prover_name
in
let
name
=
p
.
Session
.
prover_name
in
let
row
=
goals_model
#
prepend
~
parent
()
in
goals_model
#
set
~
row
~
column
:
icon_column
!
image_prover
;
goals_model
#
set
~
row
~
column
:
name_column
(
name
^
" "
^
p
.
prover_version
);
(
name
^
" "
^
p
.
Session
.
prover_version
);
(*
goals_model#set ~row ~column:visible_column true;
*)
...
...
@@ -943,7 +943,7 @@ module Helpers = struct
}
in
goals_model
#
set
~
row
~
column
:
index_column
(
Row_proof_attempt
a
);
Hashtbl
.
add
g
.
external_proofs
p
.
prover_id
a
;
Hashtbl
.
add
g
.
external_proofs
p
.
Session
.
prover_id
a
;
set_proof_state
~
obsolete
a
result
;
a
...
...
@@ -1403,12 +1403,12 @@ let redo_external_proof g a =
in
Gscheduler
.
schedule_proof_attempt
~
debug
:
(
gconfig
.
verbose
>
0
)
~
timelimit
:
gconfig
.
time_limit
~
memlimit
:
0
?
old
~
command
:
p
.
command
~
driver
:
p
.
driver
?
old
~
command
:
p
.
Session
.
command
~
driver
:
p
.
Session
.
driver
~
callback
g
.
Model
.
task
let
rec
prover_on_goal
p
g
=
let
id
=
p
.
prover_id
in
let
id
=
p
.
Session
.
prover_id
in
let
a
=
try
Hashtbl
.
find
g
.
Model
.
external_proofs
id
with
Not_found
->
...
...
@@ -1868,7 +1868,7 @@ let () =
let
add_item_provers
()
=
Util
.
Mstr
.
iter
(
fun
_
p
->
let
n
=
p
.
prover_name
^
" "
^
p
.
prover_version
in
let
n
=
p
.
Session
.
prover_name
^
" "
^
p
.
Session
.
prover_version
in
let
(
_
:
GMenu
.
image_menu_item
)
=
tools_factory
#
add_image_item
~
label
:
n
~
callback
:
(
fun
()
->
prover_on_selected_goals
p
)
...
...
@@ -2168,7 +2168,7 @@ let edit_selected_row p =
else
let
g
=
a
.
Model
.
proof_goal
in
let
t
=
g
.
Model
.
task
in
let
driver
=
a
.
Model
.
prover
.
driver
in
let
driver
=
a
.
Model
.
prover
.
Session
.
driver
in
let
file
=
match
a
.
Model
.
edited_as
with
|
""
->
...
...
@@ -2203,9 +2203,9 @@ let edit_selected_row p =
Helpers
.
set_proof_state
~
obsolete
:
false
a
res
in
let
editor
=
match
a
.
Model
.
prover
.
editor
with
match
a
.
Model
.
prover
.
Session
.
editor
with
|
""
->
gconfig
.
default_editor
|
_
->
a
.
Model
.
prover
.
editor
|
s
->
s
in
Gscheduler
.
edit_proof
~
debug
:
false
~
editor
~
file
...
...
@@ -2262,11 +2262,11 @@ let remove_proof_attempt a =
Db
.
remove_proof_attempt
a
.
Model
.
proof_db
;
let
(
_
:
bool
)
=
goals_model
#
remove
a
.
Model
.
proof_row
in
let
g
=
a
.
Model
.
proof_goal
in
Hashtbl
.
remove
g
.
Model
.
external_proofs
a
.
Model
.
prover
.
prover_id
;
Hashtbl
.
remove
g
.
Model
.
external_proofs
a
.
Model
.
prover
.
Session
.
prover_id
;
Helpers
.
check_goal_proved
g
let
remove_transf
t
=
(* TODO: remove subgoals first !!! *)
Db
.
remove_transformation
t
.
Model
.
transf_db
;
let
(
_
:
bool
)
=
goals_model
#
remove
t
.
Model
.
transf_row
in
let
g
=
t
.
Model
.
parent_goal
in
...
...
src/ide/newmain.ml
View file @
687ab81e
...
...
@@ -149,7 +149,7 @@ let gconfig =
c
.
env
<-
Lexer
.
create_env
loadpath
;
let
provers
=
Whyconf
.
get_provers
c
.
Gconfig
.
config
in
c
.
provers
<-
Util
.
Mstr
.
fold
(
Gconfig
.
get_prover_data
c
.
env
)
provers
Util
.
Mstr
.
empty
;
Util
.
Mstr
.
fold
(
Session
.
get_prover_data
c
.
env
)
provers
Util
.
Mstr
.
empty
;
c
let
()
=
...
...
@@ -442,7 +442,7 @@ let init =
|
M
.
Theory
th
->
th
.
M
.
theory
.
Theory
.
th_name
.
Ident
.
id_string
|
M
.
File
f
->
Filename
.
basename
f
.
M
.
file_name
|
M
.
Proof_attempt
a
->
let
p
=
a
.
M
.
prover
in
p
.
prover_name
^
" "
^
p
.
prover_version
p
.
Session
.
prover_name
^
" "
^
p
.
Session
.
prover_version
|
M
.
Transformation
tr
->
Session
.
transformation_id
tr
.
M
.
transf
)
let
notify
any
=
...
...
@@ -1300,7 +1300,7 @@ let () =
let
add_item_provers
()
=
Util
.
Mstr
.
iter
(
fun
_
p
->
let
n
=
p
.
prover_name
^
" "
^
p
.
prover_version
in
let
n
=
p
.
Session
.
prover_name
^
" "
^
p
.
Session
.
prover_version
in
let
(
_
:
GMenu
.
image_menu_item
)
=
tools_factory
#
add_image_item
~
label
:
n
~
callback
:
(
fun
()
->
prover_on_selected_goals
p
)
...
...
src/ide/session.ml
View file @
687ab81e
...
...
@@ -31,6 +31,25 @@ type prover_data =
mutable
editor
:
string
;
}
let
get_prover_data
env
id
pr
acc
=
try
let
dr
=
Driver
.
load_driver
env
pr
.
Whyconf
.
driver
in
Util
.
Mstr
.
add
id
{
prover_id
=
id
;
prover_name
=
pr
.
Whyconf
.
name
;
prover_version
=
pr
.
Whyconf
.
version
;
command
=
pr
.
Whyconf
.
command
;
driver_name
=
pr
.
Whyconf
.
driver
;
driver
=
dr
;
editor
=
pr
.
Whyconf
.
editor
;
}
acc
with
_e
->
eprintf
"Failed to load driver %s for prover %s. prover disabled@."
pr
.
Whyconf
.
driver
pr
.
Whyconf
.
name
;
acc
type
trans
=
|
Trans_one
of
Task
.
task
Trans
.
trans
|
Trans_list
of
Task
.
task
Trans
.
tlist
...
...
src/ide/session.mli
View file @
687ab81e
...
...
@@ -31,6 +31,10 @@ type prover_data = private
mutable
editor
:
string
;
}
val
get_prover_data
:
Env
.
env
->
Util
.
Mstr
.
key
->
Whyconf
.
config_prover
->
prover_data
Util
.
Mstr
.
t
->
prover_data
Util
.
Mstr
.
t
type
transformation_data
val
transformation_id
:
transformation_data
->
string
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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