Commit 445efda7 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'new_ide'

# Conflicts:
#	examples/bad-bts/60_at_in_tasks.mlw
#	examples/logic/einstein/why3session.xml
#	examples/logic/genealogy/why3session.xml
#	examples/regtests.sh
#	examples/tests-provers/div/why3session.xml
#	misc/ci-bench.sh
#	src/util/pp.mli
parents c5f18bbf 1623cb5f
:x: marks a potential source of incompatibility
Provers
* support for Alt-Ergo 2.0.0 (released Nov 14, 2017)
* support for Z3 4.6.0 (released Dec 18, 2017)
Standard library
* fix compatibility of theory int.Exponentiation with instances
where multiplication is not commutative.
fix corresponding realizations in Coq and Isabelle/HOL :x:
Bug fixes
* Fix issue #50:
share/Makefile.config is missing when enable_relocation=yes
Version 0.88.2, December 7, 2017
--------------------------------
......
......@@ -19,33 +19,43 @@
<prover id="14" name="Vampire" version="0.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="15" name="Alt-Ergo" version="1.00.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="16" name="veriT" version="201410" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="17" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="18" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="19" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="20" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="21" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../einstein.why" expanded="true">
<theory name="Bijection" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Einstein" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Goals" sum="59dc19f9f217c19fb5b57fc86bd98c29" expanded="true">
<goal name="G1">
<proof prover="0"><result status="timeout" time="1.00"/></proof>
<theory name="Goals" sum="9fe1211e777a560b454f17977bc1a636" expanded="true">
<goal name="G1" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="0.17"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="1.08"/></proof>
<proof prover="4"><result status="valid" time="0.88"/></proof>
<proof prover="5"><result status="timeout" time="0.99"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="1.90"/></proof>
<proof prover="9"><result status="valid" time="0.52"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="8"><result status="unknown" time="0.89"/></proof>
<proof prover="9"><result status="valid" time="0.26"/></proof>
<proof prover="10"><result status="timeout" time="2.00"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.50"/></proof>
<proof prover="15"><result status="timeout" time="1.01"/></proof>
<proof prover="15"><result status="timeout" time="2.00"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="1.17" steps="983"/></proof>
<proof prover="18"><result status="valid" time="1.41" steps="989"/></proof>
<proof prover="19"><result status="valid" time="0.21"/></proof>
<proof prover="20"><result status="valid" time="0.21"/></proof>
<proof prover="21"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="Wrong">
<proof prover="0"><result status="timeout" time="1.01"/></proof>
<goal name="Wrong" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
......@@ -53,34 +63,44 @@
<proof prover="5"><result status="timeout" time="0.99"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="1.79"/></proof>
<proof prover="8"><result status="unknown" time="0.93"/></proof>
<proof prover="9"><result status="timeout" time="1.00"/></proof>
<proof prover="10"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.01"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="unknown" time="2.07"/></proof>
<proof prover="14"><result status="unknown" time="1.00"/></proof>
<proof prover="15"><result status="unknown" time="1.33"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="unknown" time="0.57"/></proof>
<proof prover="18"><result status="unknown" time="0.66"/></proof>
<proof prover="19"><result status="timeout" time="1.00"/></proof>
<proof prover="20"><result status="timeout" time="1.00"/></proof>
<proof prover="21"><result status="unknown" time="0.07"/></proof>
</goal>
<goal name="G2">
<proof prover="0"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<goal name="G2" expl="" expanded="true">
<proof prover="0"><result status="timeout" time="1.99"/></proof>
<proof prover="1"><result status="timeout" time="2.00"/></proof>
<proof prover="2"><result status="unknown" time="0.06"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="4"><result status="timeout" time="2.00"/></proof>
<proof prover="5"><result status="timeout" time="0.99"/></proof>
<proof prover="6"><result status="timeout" time="1.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="unknown" time="1.85"/></proof>
<proof prover="9"><result status="valid" time="0.62"/></proof>
<proof prover="10"><result status="valid" time="0.79"/></proof>
<proof prover="11"><result status="timeout" time="1.00"/></proof>
<proof prover="11"><result status="timeout" time="2.00"/></proof>
<proof prover="12"><result status="timeout" time="1.00"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.27"/></proof>
<proof prover="15"><result status="valid" time="1.82" steps="523"/></proof>
<proof prover="16"><result status="timeout" time="1.00"/></proof>
<proof prover="17"><result status="valid" time="0.78" steps="1152"/></proof>
<proof prover="18"><result status="valid" time="0.95" steps="1156"/></proof>
<proof prover="19"><result status="valid" time="0.20"/></proof>
<proof prover="20"><result status="valid" time="0.18"/></proof>
<proof prover="21"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -128,9 +128,11 @@ else
echo "Counterexample regression tests succeeded. " >> $REPORT
fi
# check realizations
misc/check-realizations.sh >> $REPORT
# replay proofs
examples/regtests.sh --check-realizations &> $OUT
examples/regtests.sh &> $OUT
if test "$?" != "0" ; then
SUBJECT="$SUBJECT failed"
echo "Proof replay failed" >> $REPORT
......@@ -144,9 +146,9 @@ cp $OUT $REPORTDIR/regtests-$DATE
echo "Ending time (UTC): "`date --utc +%H:%M` >> $REPORT
# 3-line summary + 4 lines check realizations
# 3-line summary
echo "" >> $REPORT
tail -7 $OUT >> $REPORT
tail -3 $OUT >> $REPORT
echo "" >> $REPORT
# output the diff against previous run
......
......@@ -2,10 +2,6 @@
# regression tests for why3
REPLAYOPT=""
# Test realization too
CHECK_REALIZATION=""
# Don't test the rest of examples, only the realizations
ONLY_REALIZATION=""
while test $# != 0; do
case "$1" in
......@@ -19,13 +15,6 @@ case "$1" in
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
"--check-realizations")
CHECK_REALIZATION="true"
;;
"--only-realizations")
ONLY_REALIZATION="true"
CHECK_REALIZATION="true"
;;
*)
echo "$0: Unknown option '$1'"
exit 2
......@@ -35,7 +24,6 @@ done
TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
# Current directory is /examples
cd `dirname $0`
......@@ -49,41 +37,6 @@ export total=0
export sessions=""
export shapes=""
test_generated () {
# Current directory is /why3
mkdir -p $TMPREAL/lib
echo "Testing isabelle realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/isabelle/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/isabelle $TMPREAL/lib/isabelle`
if test "$TMPDIFF" = "" ; then
printf "Isabelle realizations OK\n"
else
printf "ISABELLE REALIZATIONS FAILED, please regenerate and prove them\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in /tmp. Use --only-realizations to only test realizations\n"
res=1
fi
echo "Testing coq realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/coq/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/coq $TMPREAL/lib/coq`
if test "$TMPDIFF" = "" ; then
printf "Coq realizations OK\n"
else
printf "COQ REALIZATIONS FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in /tmp. Use --only-realizations to only test realizations\n"
res=1
fi
}
run_dir () {
for f in `ls $1/*/why3session.xml`; do
......@@ -112,7 +65,6 @@ run_dir () {
shapes="$shapes $1/*/why3shapes.*"
}
if test "$ONLY_REALIZATION" = "" ; then
echo "=== Programs already ported === MUST REPLAY AND ALL GOALS PROVED ==="
echo ""
run_dir .
......@@ -163,11 +115,5 @@ echo ""
echo "Summary : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
fi
if test "$CHECK_REALIZATION" = "true" ; then
test_generated
fi
exit $res
This diff is collapsed.
# cd to the directory of this script
cd `dirname $0`
# temporary directory where we generate realizations
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
mkdir -p $TMPREAL/lib
echo "Testing isabelle realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/isabelle/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/isabelle $TMPREAL/lib/isabelle`
if test "$TMPDIFF" = "" ; then
printf "Isabelle realizations OK\n"
else
printf "ISABELLE REALIZATIONS FAILED, please regenerate and prove them\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in $TMPREAL\n"
res=1
fi
echo "Testing coq realizations"
# First copy current realizations in a tmp directory
cp -r ../lib/coq/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' -x '*~' -x '*.aux' ../lib/coq $TMPREAL/lib/coq`
if test "$TMPDIFF" = "" ; then
printf "Coq realizations OK\n"
else
printf "COQ REALIZATIONS FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realizations are in $TMPREAL\n"
res=1
fi
......@@ -29,4 +29,4 @@ bin/why3config --detect-provers
make bench
# check that the realizations are ok (temporarily disabled)
# examples/regtests.sh --only-realizations
# misc/check_realizations.sh
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-2.2.0"
exec = "alt-ergo-1.30"
exec = "alt-ergo-1.01"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "1.30"
version_ok = "2.0.0"
version_old = "1.30"
version_old = "1.01"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
......@@ -347,14 +349,16 @@ version_old = "201310"
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.6.0"
version_ok = "4.5.0"
version_ok = "4.4.1"
version_ok = "4.4.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_440"
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
......@@ -365,14 +369,16 @@ use_at_auto_level = 1
name = "Z3"
alternative = "noBV"
exec = "z3"
exec = "z3-4.6.0"
exec = "z3-4.5.0"
exec = "z3-4.4.1"
exec = "z3-4.4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.6.0"
version_ok = "4.5.0"
version_ok = "4.4.1"
version_ok = "4.4.0"
version_old = "4.4.1"
version_old = "4.4.0"
driver = "z3_432"
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
......
......@@ -31,16 +31,19 @@ let localdir = $localdir
let compile_time_support = [ @COMPILETIMECOQ@ @COMPILETIMEPVS@ ]
" > $config
if [ "@enable_relocation@" = "no" ]; then
echo "
BINDIR = $bindir
LIBDIR = $libdir
DATADIR = $datadir
OCAMLBEST = @OCAMLBEST@
BIGINTLIB = @BIGINTLIB@
INCLUDE = @BIGINTINCLUDE@ -I @OCAMLINSTALLLIB@/why3
INCLUDEALL = @BIGINTINCLUDE@ @ZIPINCLUDE@ @MENHIRINCLUDE@ -I @OCAMLINSTALLLIB@/why3
" > $makefileconfig
if [ "@enable_relocation@" = "no" ]; then
echo "
BINDIR = $bindir
LIBDIR = $libdir
DATADIR = $datadir
" >> $makefileconfig
fi
......@@ -61,9 +61,9 @@ type prover_autodetection_data =
execs : string list;
version_switch : string;
version_regexp : string;
versions_ok : Str.regexp list;
versions_old : Str.regexp list;
versions_bad : Str.regexp list;
versions_ok : (string * Str.regexp) list;
versions_old : (string * Str.regexp) list;
versions_bad : (string * Str.regexp) list;
(** If none it's a fake prover (very bad version) *)
prover_command : string option;
prover_command_steps : string option;
......@@ -84,7 +84,7 @@ let prover_keys =
let load_prover kind (id,section) =
check_exhaustive section prover_keys;
let reg_map = List.rev_map why3_regexp_of_string in
let reg_map = List.rev_map (fun s -> (s,why3_regexp_of_string s)) in
let prover = { kind = kind;
prover_id = id;
prover_name = get_string section "name";
......@@ -158,7 +158,7 @@ type env =
unknown version (neither good or bad)
| None there is a good version *)
prover_unknown_version :
(int * string * config_prover) option Hstr.t;
(prover_autodetection_data * int * string * config_prover) option Hstr.t;
(* string -> priority * prover *)
prover_shortcuts : (int * prover) Hstr.t;
mutable possible_prover_shortcuts : (filter_prover * string) list;
......@@ -254,15 +254,15 @@ let ask_prover_version env exec_name version_switch =
Hstr2.add env.prover_output (exec_name,version_switch) res;
res
let check_version version schema = Str.string_match schema version 0
let check_version version (_,schema) = Str.string_match schema version 0
let known_version env exec_name =
Hstr.replace env.prover_unknown_version exec_name None
let unknown_version env exec_name prover_id prover_config priority =
let unknown_version env exec_name prover_id prover_config data priority =
if not (Hstr.mem env.prover_unknown_version exec_name)
then Hstr.replace env.prover_unknown_version exec_name
(Some (priority,prover_id,prover_config))
(Some (data,priority,prover_id,prover_config))
let empty_alt s = if s = "" then "alt" else s
......@@ -510,22 +510,29 @@ let detect_exec env data acc exec_name =
if level > 0 then record_prover_for_auto_mode prover level;
add_prover_with_uniq_id prover_config acc
end
else (unknown_version env exec_name data.prover_id prover_config priority;
else (unknown_version env exec_name data.prover_id prover_config data priority;
acc)
let detect_prover env acc data =
List.fold_left (detect_exec env data) acc data.execs
let pp_versions =
Pp.print_list Pp.comma
(Pp.print_pair_delim Pp.nothing Pp.nothing Pp.nothing Pp.string Pp.nothing)
(** add the prover unknown *)
let detect_unknown env detected =
Hstr.fold (fun _ pc acc ->
match pc with
| None -> acc
| Some (priority,prover_id,prover_config) ->
| Some (prover_data,priority,prover_id,prover_config) ->
let prover = prover_config.prover in
Warning.emit "Warning: prover %s version %s is not known to be \
supported.@."
prover.Wc.prover_name prover.prover_version;
Warning.emit "@[Prover %s version %s is not known to be supported.@\n\
Known versions for this prover:@ %a@\n\
Known old versions for this prover:@ %a@]@."
prover.Wc.prover_name prover.prover_version
pp_versions prover_data.versions_ok
pp_versions prover_data.versions_old;
(* Pb: Even if it match the first prover section (normally
highest priority) since it is unknown it has the lower
priority for its id as shortcut. Perhaps we don't want
......
......@@ -928,7 +928,12 @@ let absolute_driver_file main s =
let load_driver main env file extras =
let file = absolute_driver_file main file in
Driver.load_driver_absolute env file extras
try
Driver.load_driver_absolute env file extras
with e ->
eprintf "Fatal error while loading driver file '%s': %a@."
file Exn_printer.exn_printer e;
exit 1
let unknown_to_known_provers provers pu =
......
......@@ -573,7 +573,6 @@ let interpNotif (n: notification) =
PE.error_print_msg
(Format.asprintf "Query error on selected node: \"%s\"" s)
| Query_Info (_nid, s) -> PE.error_print_msg s
| Help s -> PE.error_print_msg s
| Information s -> PE.error_print_msg s
| Error s ->
PE.error_print_msg
......
......@@ -195,23 +195,6 @@ let env, gconfig = try
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(* Initialization of config, provers, task_driver and controller in the server *)
let () =
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
Server.init_server gconfig.config env dir;
Queue.iter (fun f -> send_request (Add_file_req f)) files
let () =
Debug.dprintf debug "Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
Debug.dprintf debug " done.@.";
Gconfig.init ()
(********************************)
......@@ -377,6 +360,30 @@ let update_label_saved (label: GMisc.label) =
(* Graphical elements *)
(**********************)
let initialization_complete = ref false
let warnings = Queue.create ()
let record_warning ?loc msg =
Format.eprintf "%awarning: %s@."
(Pp.print_option Loc.report_position) loc msg;
Queue.push (loc,msg) warnings
let () =
Warning.set_hook record_warning;
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
Server.init_server gconfig.config env dir;
Queue.iter (fun f -> send_request (Add_file_req f)) files;
send_request Get_global_infos;
Debug.dprintf debug "Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
Debug.dprintf debug " done.@.";
Gconfig.init ()
let main_window : GWindow.window =
let w = GWindow.window
......@@ -393,7 +400,8 @@ let main_window : GWindow.window =
(fun {Gtk.width=w;Gtk.height=h} ->
gconfig.window_height <- h;
gconfig.window_width <- w)
in w
in
w
(* the main window contains a vertical box, containing:
1. the menu [menubar]
......@@ -477,13 +485,6 @@ let provers_factory =
(****************************)
(***********************************)
(* connection of actions to signals *)
(***********************************)
......@@ -1003,12 +1004,47 @@ let print_message ~kind ~notif_kind fmt =
add_to_log notif_kind s;
if kind>0 then
begin
message_zone#buffer#set_text s;
message_zone#buffer#insert (s ^ "\n");
messages_notebook#goto_page error_page
end)
str_formatter
fmt
let display_warnings () =
if Queue.is_empty warnings then () else
begin
let nwarn = ref 0 in
begin try
Queue.iter
(fun (loc,msg) ->
if !nwarn = 4 then
begin
Format.fprintf Format.str_formatter "[%d more warnings. See stderr for details]@\n" (Queue.length warnings - !nwarn);
raise Exit
end
else
begin
incr nwarn;
match loc with
| None ->
Format.fprintf Format.str_formatter "%s@\n@\n" msg
| Some l ->
(* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
Format.fprintf Format.str_formatter "%a: %s@\n@\n"
Loc.gen_report_position l msg
end) warnings;
with Exit -> ();
end;
Queue.clear warnings;
let msg =
Format.flush_str_formatter ()
in
print_message ~kind:1 ~notif_kind:"warning" "%s" msg
end
let () =
Warning.set_hook (fun ?loc s -> record_warning ?loc s; display_warnings ())
(**** Monitor *****)
......@@ -1591,8 +1627,6 @@ let (_ : GtkSignal.id) =
(* Notification Handling *)
(*************************)
let initialization_complete = ref false
let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) ->
......@@ -1625,11 +1659,7 @@ let treat_message_notification msg = match msg with
print_message ~kind:1 ~notif_kind:"Query_info" "%s" s
| Query_Error (_id, s) ->
print_message ~kind:1 ~notif_kind:"Query_error" "%s" s
| Help s ->
print_message ~kind:1 ~notif_kind:"Help" "%s" s
| Information s ->
if not !initialization_complete then main_window#show ();
initialization_complete := true;
print_message ~kind:1 ~notif_kind:"Information" "%s" s
| Task_Monitor (t, s, r) -> update_monitor t s r
| Open_File_Error s ->
......@@ -1637,7 +1667,6 @@ let treat_message_notification msg = match msg with
| Parse_Or_Type_Error (loc, rel_loc, s) ->
if gconfig.allow_source_editing || !initialization_complete then
begin
if not !initialization_complete then main_window#show ();
(* TODO find a new color *)
scroll_to_loc ~force_tab_switch:true (Some (rel_loc,0));
color_loc ~color:Goal_color rel_loc;
......@@ -2205,7 +2234,9 @@ let treat_notification n =
Hint.remove node_id_proved id;
Hint.remove node_id_pa id
| Initialized g_info ->
(* TODO: treat other *)
initialization_complete := true;
main_window#show ();
display_warnings ();
init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
| Saved ->
session_needs_saving := false;
......
......@@ -42,7 +42,6 @@ type message_notification =
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Parse_Or_Type_Error of Loc.position * Loc.position * string
......@@ -117,13 +116,15 @@ type ide_request =
| Reload_req
| Exit_req
| Interrupt_req
| Get_global_infos
(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
match r with
| Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
| Reload_req -> true
| Set_config_param _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Save_req | Exit_req
| Save_req | Exit_req | Get_global_infos
| Interrupt_req | Focus_req _ | Unfocus_req -> false
......@@ -43,7 +43,6 @@ type message_notification =
| Replay_Info of string
| Query_Info of node_ID * string