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
354f4c0a
Commit
354f4c0a
authored
Oct 11, 2017
by
MARCHE Claude
Browse files
replace use of eprintf by proper debug.dprintf
parent
cb83244e
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/ide/why3ide.ml
View file @
354f4c0a
...
...
@@ -1043,7 +1043,8 @@ let scroll_to_loc ~force_tab_switch loc_of_goal =
try
let
(
n
,
v
,
_
,
_
)
=
get_source_view_table
f
in
if
force_tab_switch
then
(
eprintf
"tab switch to page %d@."
n
;
notebook
#
goto_page
n
);
(
Debug
.
dprintf
debug
"tab switch to page %d@."
n
;
notebook
#
goto_page
n
);
move_to_line
~
yalign
:
0
.
0
v
l
with
Nosourceview
_
->
()
...
...
src/session/controller_itp.ml
View file @
354f4c0a
...
...
@@ -445,9 +445,6 @@ let timeout_handler () =
try
build_prover_call
?
proof_script
~
cntexample
c
id
pr
limit
callback
ores
with
e
when
not
(
Debug
.
test_flag
Debug
.
stack_trace
)
->
(*Format.eprintf
"@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
Exn_printer.exn_printer e;*)
callback
(
InternalFailure
e
)
done
with
Queue
.
Empty
->
()
...
...
@@ -728,8 +725,7 @@ let schedule_transformation c id name args ~callback ~notification =
(* if result is same as input task, consider it as a failure *)
callback
(
TSfailed
(
id
,
Noprogress
))
|
e
(* when not (Debug.test_flag Debug.stack_trace) *)
->
(* Format.eprintf
"@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
(* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
name Exn_printer.exn_printer e; TODO *)
callback
(
TSfailed
(
id
,
e
))
end
;
...
...
src/session/itp_server.ml
View file @
354f4c0a
...
...
@@ -388,7 +388,7 @@ let () =
let
get_server_data
()
=
match
!
server_data
with
|
None
->
Format
.
eprintf
"not yet initialized@."
;
Format
.
eprintf
"
get_server_data(): fatal error, server
not yet initialized@."
;
exit
1
|
Some
x
->
x
...
...
@@ -620,14 +620,13 @@ end
with
Invalid_argument
s
->
P
.
notify
(
Message
(
Error
s
))
(* Send source file from the controller to the IDE even if the controller's
status is not correct *)
(* Send all source files from the controller session to the IDE *)
let
load_files_session
()
=
let
d
=
get_server_data
()
in
let
s
=
d
.
cont
.
controller_session
in
let
files
=
Session_itp
.
get_files
s
in
Stdlib
.
Hstr
.
iter
(
fun
_
f
->
Format
.
eprintf
"File :
%s@."
(
file_name
f
);
Debug
.
dprintf
debug
"load_files_session: loading '
%s
'
@."
(
file_name
f
);
read_and_send
(
file_name
f
))
files
let
relativize_location
s
loc
=
...
...
@@ -663,19 +662,6 @@ end
P
.
notify
(
Message
(
Parse_Or_Type_Error
(
Loc
.
dummy_position
,
s
)));
false
(*
let task_driver config env =
try
let main = Whyconf.get_main config in
let d = "why3_itp" in
let d = Whyconf.load_driver main env d [] in
Debug.dprintf debug "driver for task printing loaded@.";
d
with e ->
Format.eprintf "Fatal error while loading itp driver: %a@." Exn_printer.exn_printer e;
exit 1
*)
(* ----------------------------------- ------------------------------------- *)
let
get_node_type
(
node
:
any
)
=
...
...
@@ -1054,7 +1040,7 @@ end
P
.
notify
(
Node_change
(
node_ID
,
Proof_status_change
(
res
,
obs
,
limit
)))
|
_
->
()
with
Not_found
when
not
(
Debug
.
test_flag
Debug
.
stack_trace
)
->
Format
.
eprintf
"
A
nomaly
:
Itp_server.notify_change_proved@."
;
Format
.
eprintf
"
Fatal a
nomaly
in
Itp_server.notify_change_proved@."
;
exit
1
let
schedule_proof_attempt
~
counterexmp
nid
(
p
:
Whyconf
.
config_prover
)
limit
=
...
...
src/session/server_utils.ml
View file @
354f4c0a
...
...
@@ -71,20 +71,19 @@ let cont_from_session ~notify cont f : bool option =
(* Case of user giving a file that gets chopped to an other file *)
if not (Sys.is_directory dir) then
begin
let s = "Not a directory: " ^ dir in
Format.eprintf "%s@." s;
Format.eprintf "Not a directory: %s@." dir;
exit 1
end
end
else
begin
Format.
e
printf
"[session server info]
'%s' does not exist. \
Creating directory of that name for the
project
@." dir;
Format.
d
printf
debug "
'%s' does not exist. \
Creating directory of that name for the
Why3 session
@." dir;
Unix.mkdir dir 0o777
end;
(* we load the session *)
let ses,use_shapes = load_session dir in
Format.
e
printf
"[session server info]
using shapes: %b@." use_shapes;
Format.
d
printf
debug "
using shapes: %b@." use_shapes;
(* temporary, this should not be donne like this ! *)
Controller_itp.set_session cont ses;
(* update the session *)
...
...
@@ -152,7 +151,7 @@ let load_strategies cont =
Stdlib
.
Hstr
.
add
cont
.
Controller_itp
.
controller_strategies
shortcut
(
name
,
st
.
Whyconf
.
strategy_desc
,
code
)
with
Strategy_parser
.
SyntaxError
msg
->
Format
.
eprintf
"
[ERROR] L
oading strategy '%s' failed: %s@."
name
msg
;
Format
.
eprintf
"
Fatal: l
oading strategy '%s' failed: %s@."
name
msg
;
exit
1
)
strategies
...
...
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