Commit 6cbc43d8 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'batch_mode_cursor' into 'master'

batch mode: add printing of source color and cursor position as text

See merge request !124
parents abdb518d 575017d9
#!/bin/bash
dir=`dirname $0`
updateoracle=false
files=""
success=true
while test $# != 0; do
case "$1" in
"-update-oracle")
updateoracle=true;;
"-"*)
printf "unknown option: %s\n" "$1"
printf "usage: ide-bench [-update-oracle] <files>\n"
printf " <files> must be given with the '.mlw' suffix\n"
printf " if <files> empty, use all files from directory 'ide'\n"
exit 2;;
*)
files="$files $1"
esac
shift
done
if test "$files" = "" ; then
files="$dir/ide/*.mlw"
fi
# $1 = dir, $2 = filename
run () {
printf "$2..."
file_path="$1/$2"
oracle_file="$1/oracles/$2.oracle"
echo "$file_path"
xvfb-run bin/why3ide --batch "down;down;color;" "${file_path}.mlw" > "${file_path}.out"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "${file_path}.out")
if [ "$str_oracle" = "$str_out" ] ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for ${file_path}"
mv "${file_path}.out" "${oracle_file}"
else
echo "FAILED!"
echo "Oracle is ${str_oracle}"
echo "Output is ${str_out}"
echo "diff is the following:"
echo "${file_path}"
diff "${oracle_file}" "${file_path}.out"
success=false
fi
fi
}
for file in $files; do
filedir=`dirname $file`
filebase=`basename $file .mlw`
run $filedir $filebase
done
if $success; then
exit 0
else
exit 1
fi
module M
use int.Int
use ref.Ref
use map.Map
let ghost test_map (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let ghost test_map_multidim1 (ghost x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
let ghost test_map_multidim2 (ghost x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
let ghost proj_map_test1 (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
let ghost proj_map_test2 (ghost x : ref (map int bool)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 true
end
theory ModelMap
use map.Map
goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
end
module OtherIndices
use map.Map
goal g : forall m: map real real. m 0.1 = 0.0 \/ m 0.2 = m 0.1
end
\ No newline at end of file
Cursor is placed at position: (7, 0)
Recorded colors on the source code are:
Color "goal_tag" from (6, 12) to (6, 20)
Color "goal_tag" from (7, 14) to (7, 28)
Color "premise_tag" from (9, 4) to (9, 23)
End color
......@@ -16,6 +16,8 @@ do
;;
ide)
WHY3CONFIG="" xvfb-run bin/why3 ide --batch "" examples/logic/einstein.why
bin/why3config --detect-provers
bench/ide-bench
;;
doc)
make doc
......
......@@ -2520,6 +2520,31 @@ let () =
(* simulate some user actions and take screenshots *)
(***************************************************)
let pos_cursor_and_color (v:GSourceView.source_view) =
let buf = v#source_buffer in
let iter = buf#get_iter_at_mark `INSERT in
let line, column = iter#line + 1, iter#line_index in
(* This is the line that corresponds to the goal *)
Format.printf "Cursor is placed at position: (%d, %d)@."
line column;
let iter = ref buf#start_iter in
Format.printf "Recorded colors on the source code are:@.";
while not (!iter#is_end) do
let l = !iter#get_toggled_tags true in
if l = [] then
()
else
List.iter (fun (tag: GText.tag) ->
let tag_name = tag#get_property GtkText.Tag.P.name in
if tag_name <> "" then
let iter2 = !iter#forward_to_tag_toggle (Some tag) in
Format.printf "Color \"%s\" from (%d, %d) to (%d, %d)@."
tag_name !iter#line !iter#line_index iter2#line iter2#line_index)
l;
iter := !iter#forward_char;
done;
Format.printf "End color@."
let batch s =
let cmd = ref (Strings.split ';' s) in
let last = ref (Sys.time ()) in
......@@ -2553,6 +2578,18 @@ let batch s =
let cmd = Strings.join " " cmd in
let cmd = Printf.sprintf "import -window \"%s\" -define png:include-chunk=none %s" window_title cmd in
if Sys.command cmd <> 0 then Printf.eprintf "Batch command failed: %s\n%!" cmd
| "color" :: cmd ->
begin
let cmd = Strings.join " " cmd in
let v = Hstr.fold (fun _ x acc ->
match acc, x with
| None, (sp, sv, _, _) when sp = 1 ->
Some sv
| _ -> acc) source_view_table None
in
Opt.iter pos_cursor_and_color v;
interp cmd
end
| ["save"] -> send_request Save_req
| _ -> Printf.eprintf "Unrecognized batch command: %s\n%!" c
end;
......
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