Commit d92706f7 authored by David Hauzar's avatar David Hauzar

Displaying of counterexamples enhanced.

When counterexample is displayed interleaved with source code, only the
part of the source code from the beginning to the line of the last
counterexample element is displayed and the focus in the editor is on the
end of that source code.
Textual counterexample (without interleaving with source code) is not
displayed by default. There is a debug flag debug_show_text_cntexmp that
enables such display.
parent f7093a76
......@@ -289,13 +289,22 @@ let interleave_with_source
~filename
~source_code =
try
let model_file = StringMap.find filename model.model_files in
let lines = Str.split (Str.regexp "^") source_code in
let model_file = StringMap.find filename model.model_files in
let src_lines_up_to_last_cntexmp_el source_code model_file =
let (last_cntexmp_line, _) = IntMap.max_binding model_file in
let lines = Str.bounded_split (Str.regexp "^") source_code (last_cntexmp_line+1) in
let remove_last_element list =
let list_rev = List.rev list in
match list_rev with
| _ :: tail -> List.rev tail
| _ -> List.rev list_rev
in
remove_last_element lines in
let (source_code, _) = List.fold_left
(interleave_line
start_comment end_comment me_name_trans model_file)
("", 1)
lines in
(src_lines_up_to_last_cntexmp_el source_code model_file) in
source_code
with Not_found ->
source_code
......
......@@ -33,6 +33,9 @@ let () = reset_gc ()
let debug = Debug.lookup_flag "ide_info"
let debug_show_text_cntexmp = Debug.register_info_flag "show_text_cntexmp"
~desc:"Print@ textual@ counterexample@ before@ printing@ counterexample@ interleaved@ with@ cource@ code."
(************************)
(* parsing command line *)
(************************)
......@@ -643,13 +646,19 @@ let update_tabs a =
match a.S.proof_state with
| S.Done r ->
if not (Model_parser.is_model_empty r.Call_provers.pr_model) then begin
"Counterexample:\n" ^
(Model_parser.model_to_string r.Call_provers.pr_model) ^
"\n\nSource code interleaved with counterexample:" ^
let cntexample_text =
if Debug.test_flag debug_show_text_cntexmp then
"Counterexample:\n" ^
(Model_parser.model_to_string r.Call_provers.pr_model) ^
"\n\nSource code interleaved with counterexample:"
else
"" in
let cntexample_text = cntexample_text ^
(Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
~source_code:(Sysutil.file_contents !current_file))
~source_code:(Sysutil.file_contents !current_file)) in
cntexample_text
end else
""
| _ -> ""
......@@ -670,6 +679,7 @@ let update_tabs a =
edited_view#scroll_to_mark `INSERT;
output_view#source_buffer#set_text output_text;
counterexample_view#source_buffer#set_text counterexample_text;
counterexample_view#scroll_to_mark `INSERT;
......
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