Skip to content

GitLab

why3
why3
Commit a02d4770 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Merge branch 'itp' of git+ssh://scm.gforge.inria.fr/git/why3/why3 into itp

parents a785ec55 7f929788
Hide whitespace changes
Inline Side-by-side
Showing with 134 additions and 58 deletions
src/ide/why3ide.ml
View file @ a02d4770
......@@ -751,10 +751,32 @@ let task_view =
~packing:scrolled_task_view#add
()
(* TODO is it necessary ?
let pr_output_page,scrolled_pr_output_view =
let label = GMisc.label ~text:"Prover output" () in
1, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let scrolled_pr_output_view =
GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~shadow_type:`ETCHED_OUT
~packing:scrolled_pr_output_view#add ()
(* Showing prover output *)
let prover_output_view =
GSourceView2.source_view
~editable:false
~cursor_visible:true
~show_line_numbers:true
~packing:scrolled_pr_output_view#add
()
*)
(* Creating a page for source code view *)
let create_source_view =
(* Counter for pages *)
let n = ref 1 in
let n = ref 2 in
(* Create a page with tabname [f] and buffer equal to [content] in the
notebook. Also add a corresponding page in source_view_table. *)
let create_source_view f content =
......@@ -951,7 +973,7 @@ let convert_color (color: color): string =
| Goal_color -> "goal_tag"
let move_to_line ~yalign (v : GSourceView2.source_view) line =
let line = max 0 line in
let line = max 0 (line - 1) in
let line = min line v#buffer#line_count in
let it = v#buffer#get_iter (`LINE line) in
v#buffer#place_cursor ~where:it;
......@@ -1203,6 +1225,25 @@ let on_selected_row r =
task_view#source_buffer#set_text ""
else
send_request (Get_task id)
| NProofAttempt ->
let (pa, _obs, _l) = Hint.find node_id_pa id in
(match pa with
| Controller_itp.Done pr ->
task_view#source_buffer#set_text pr.Call_provers.pr_output
| Controller_itp.Unedited ->
task_view#source_buffer#set_text "Unedited"
| Controller_itp.JustEdited ->
task_view#source_buffer#set_text "Just edited"
| Controller_itp.Interrupted ->
task_view#source_buffer#set_text "Interrupted"
| Controller_itp.Scheduled ->
task_view#source_buffer#set_text "Scheduled"
| Controller_itp.Running ->
task_view#source_buffer#set_text "Running"
| Controller_itp.InternalFailure _e ->
task_view#source_buffer#set_text "Internal failure"
| Controller_itp.Uninstalled _p ->
task_view#source_buffer#set_text "Uninstalled")
| _ -> send_request (Get_task id)
with
| Not_found -> task_view#source_buffer#set_text ""
......@@ -1394,18 +1435,23 @@ let open_session: GMenu.menu_item =
let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) -> print_message "%s" s
| Transf_error (_id, s) -> print_message "%s" s
| Strat_error (_id, s) -> print_message "%s" s
| Replay_Info s -> print_message "%s" s
| Query_Info (_id, s) -> print_message "%s" s
| Query_Error (_id, s) -> print_message "%s" s
| Help s -> print_message "%s" s
| Information s -> print_message "%s" s
| Task_Monitor (t, s, r) -> update_monitor t s r
| Open_File_Error s -> print_message "%s" s
| Parse_Or_Type_Error s -> print_message "%s" s
| File_Saved f ->
| Proof_error (_id, s) -> print_message "%s" s
| Transf_error (_id, s) -> print_message "%s" s
| Strat_error (_id, s) -> print_message "%s" s
| Replay_Info s -> print_message "%s" s
| Query_Info (_id, s) -> print_message "%s" s
| Query_Error (_id, s) -> print_message "%s" s
| Help s -> print_message "%s" s
| Information s -> print_message "%s" s
| Task_Monitor (t, s, r) -> update_monitor t s r
| Open_File_Error s -> print_message "%s" s
| Parse_Or_Type_Error (loc, s) ->
begin
(* TODO find a new color *)
color_loc ~color:Goal_color loc;
print_message "%s" s
end
| File_Saved f ->
begin
try
let (_source_page, _source_view, b, l) = Hstr.find source_view_table f in
......@@ -1413,10 +1459,10 @@ let treat_message_notification msg = match msg with
update_label_saved l;
print_message "%s was saved" f
with
| Not_found ->
| Not_found ->
print_message "Please report: %s was not found in ide but was saved in session" f
end
| Error s ->
| Error s ->
if Debug.test_flag debug then
print_message "%s" s
else
......@@ -1574,11 +1620,11 @@ let treat_notification n =
begin
match uinfo with
| Proved b ->
Hint.replace node_id_proved id b;
set_status_column (get_node_row id)#iter;
(* Trying to move cursor on first unproven goal around on all cases
but not when proofAttempt is updated because ad hoc debugging. *)
send_request (Get_first_unproven_node id)
Hint.replace node_id_proved id b;
set_status_column (get_node_row id)#iter;
(* Trying to move cursor on first unproven goal around on all cases
but not when proofAttempt is updated because ad hoc debugging. *)
send_request (Get_first_unproven_node id)
| Proof_status_change (pa, obs, l) ->
let r = get_node_row id in
Hint.replace node_id_pa id (pa, obs, l);
......
src/session/itp_communication.ml
View file @ a02d4770
......@@ -32,7 +32,7 @@ type message_notification =
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Parse_Or_Type_Error of string
| Parse_Or_Type_Error of Loc.position * string
| File_Saved of string
| Error of string
| Open_File_Error of string
......
src/session/itp_communication.mli
View file @ a02d4770
......@@ -33,13 +33,13 @@ type message_notification =
| Help of string
(* General information *)
| Information of string
(* Number of task scheduled, running, etc *)
(* Number of task scheduled, running, etc *)
| Task_Monitor of int * int * int
(* A file was read or reloaded and now contains a parsing or typing error *)
| Parse_Or_Type_Error of string
(* An error happened that could not be identified in server *)
| File_Saved of string
| Parse_Or_Type_Error of Loc.position * string
(* [File_Saved f] f was saved *)
| File_Saved of string
(* An error happened that could not be identified in server *)
| Error of string
| Open_File_Error of string
......
src/session/itp_server.ml
View file @ a02d4770
......@@ -273,19 +273,19 @@ let print_request fmt r =
let print_msg fmt m =
match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
| Transf_error (_ids, s) -> fprintf fmt "transf error %s" s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
| Query_Error (_ids, s) -> fprintf fmt "query error %s" s
| Help _s -> fprintf fmt "help"
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Parse_Or_Type_Error s -> fprintf fmt "parse_or_type_error:\n %s" s
| File_Saved s -> fprintf fmt "file saved %s" s
| Error s -> fprintf fmt "%s" s
| Open_File_Error s -> fprintf fmt "%s" s
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
| Transf_error (_ids, s) -> fprintf fmt "transf error %s" s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
| Query_Error (_ids, s) -> fprintf fmt "query error %s" s
| Help _s -> fprintf fmt "help"
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Parse_Or_Type_Error (_, s) -> fprintf fmt "parse_or_type_error:\n %s" s
| File_Saved s -> fprintf fmt "file saved %s" s
| Error s -> fprintf fmt "%s" s
| Open_File_Error s -> fprintf fmt "%s" s
(* TODO ad hoc printing. Should reuse print_loc. *)
let print_loc fmt (loc: Loc.position) =
......@@ -553,6 +553,14 @@ module P = struct
let get_requests = Pr.get_requests
(* true if nid is below f_node or does not exists (in which case the
notification is a remove). false if not below. *)
let is_below s nid f_node =
let any = try Some (any_from_node_ID nid) with _ -> None in
match any with
| None -> true
| Some any -> Session_itp.is_below s any f_node
let notify n =
let d = get_server_data() in
let s = d.cont.controller_session in
......@@ -562,10 +570,8 @@ module P = struct
let updated_node = get_modified_node n in
match updated_node with
| None -> Pr.notify n
| Some nid when
let any = any_from_node_ID nid in
Session_itp.is_below s any f_node ->
Pr.notify n
| Some nid when is_below s nid f_node ->
Pr.notify n
| _ -> ()
end
......@@ -604,20 +610,38 @@ end
Format.eprintf "File : %s@." f.file_name;
read_and_send f.file_name) files
let relativize_location s loc =
let f, l, b, e = Loc.get loc in
let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
Loc.user_position f l b e
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
try reload_files cont ~use_shapes; true with
| Loc.Located (loc, e) ->
let loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a at %a@."
Exn_printer.exn_printer e Pretty.print_loc loc in
P.notify (Message (Parse_Or_Type_Error (loc, s)));
false
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s));
P.notify (Message (Parse_Or_Type_Error (Loc.dummy_position, s)));
false
let add_file c ?format fname =
try add_file c ?format fname; true with
let add_file cont ?format fname =
try add_file cont ?format fname; true with
| Loc.Located (loc, e) ->
let loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a at %a@."
Exn_printer.exn_printer e Pretty.print_loc loc in
P.notify (Message (Parse_Or_Type_Error (loc, s)));
false
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s)); false
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error (Loc.dummy_position, s)));
false
let task_driver config env =
try
......
src/session/json_util.ml
View file @ a02d4770
......@@ -247,6 +247,13 @@ let convert_constructor_message (m: message_notification) =
| Open_File_Error _ -> String "Open_File_Error"
| File_Saved _ -> String "File_Saved"
let convert_loc (loc: Loc.position) : Json_base.json =
let (file, line, col1, col2) = Loc.get loc in
Record (convert_record ["file", Json_base.String file;
"line", Json_base.Int line;
"col1", Json_base.Int col1;
"col2", Json_base.Int col2])
let convert_message (m: message_notification) =
let cc = convert_constructor_message in
Record (match m with
......@@ -282,9 +289,10 @@ let convert_message (m: message_notification) =
| Task_Monitor (n, k, p) ->
convert_record ["mess_notif", cc m;
"monitor", List [Int n; Int k; Int p]]
| Parse_Or_Type_Error s ->
| Parse_Or_Type_Error (loc, s) ->
convert_record ["mess_notif", cc m;
"error", String s]
"loc", convert_loc loc;
"error", String s]
| Error s ->
convert_record ["mess_notif", cc m;
"error", String s]
......@@ -302,13 +310,6 @@ let convert_color (color: color) : Json_base.json =
| Premise_color -> "Premise_color"
| Goal_color -> "Goal_color")
let convert_loc (loc: Loc.position) : Json_base.json =
let (file, line, col1, col2) = Loc.get loc in
Record (convert_record ["file", Json_base.String file;
"line", Json_base.Int line;
"col1", Json_base.Int col1;
"col2", Json_base.Int col2])
let convert_loc_color (loc,color: Loc.position * color) : Json_base.json =
let loc = convert_loc loc in
let color = convert_color color in
......@@ -686,6 +687,11 @@ let parse_message constr j =
let s = get_string (get_field j "open_error") in
Open_File_Error s
| "Parse_Or_Type_Error" ->
let loc = parse_loc (get_field j "loc") in
let error = get_string (get_field j "error") in
Parse_Or_Type_Error (loc, error)
| _ -> raise NotMessage
......
src/tools/why3shell.ml
View file @ a02d4770
......@@ -108,7 +108,7 @@ g -> print the current task\n\
p -> print the session@." s
| Information s -> fprintf fmt "%s@." s
| Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
| Parse_Or_Type_Error s -> fprintf fmt "%s@." s
| Parse_Or_Type_Error (_, s) -> fprintf fmt "%s@." s
| Error s ->
fprintf fmt "%s@." s
| Open_File_Error s -> fprintf fmt "%s@." s
......
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