Commit 025c5e94 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'ctrl_l' into 'master'

Ide/itp_server: experimental ctrl-C ctrl-L (àla merlin)

See merge request !242
parents f82143b1 6d6acfdd
......@@ -35,6 +35,9 @@ API
* ITP constructor `Source_and_ce` now has 3 arguments instead of 2 :x:
* ITP constructors `File_contents` and `Source_and_ce` has a new argument for
the file format :x:
* ITP constructor `File_contents` has a new boolean argument for
interpretation of the file in the IDE as `read_only` :x:
* New ITP constructor `Ident_notif_loc`
Transformations
* `apply`/`rewrite` behaves better in presence of `let`;
......@@ -65,6 +68,10 @@ IDE
* strategies can now be defined using `%t` (resp. `%m`) to call a prover with
the default timelimit (resp. memlimit)
* added minimal search menu
* A merlin-like feature to find the ident located under the cursor has been
added in the Edit menu.
* Read only file can now be displayed and removed by right clicking on their
tab titles
Realizations
* added experimental realizations for new Set theories in both Isabelle and Coq
......
......@@ -553,10 +553,12 @@ let interpNotif (n: notification) =
TaskList.attach_new_node nid parent ntype name detached;
TaskList.onclick_do_something (string_of_int nid);
sendRequest (Get_task (string_of_int nid))
| File_contents (_f,_s,_) ->
| File_contents (_f,_s,_, _) ->
PE.error_print_msg "Notification File_contents not handled yet"
| Source_and_ce _ ->
PE.error_print_msg "Notification Source_and_ce not handled yet"
| Ident_notif_loc _ ->
PE.error_print_msg "Notification Ident_notif_loc not handled yet"
| Next_Unproven_Node_Id (_nid1,_nid2) ->
PE.error_print_msg "Notification Next_Unproven_Node_Id not handled yet"
| Task (nid, task, _list_loc, _goal_loc, _lang) -> (* TODO add color on sources *)
......
This diff is collapsed.
......@@ -107,11 +107,13 @@ type notification =
- [goal_loc] the location of the goal,
- [lang] the language to load in Why3ide for syntax coloring
*)
| File_contents of string * string * Env.fformat
(* File_contents (filename, contents, format) *)
| File_contents of string * string * Env.fformat * bool
(* File_contents (filename, contents, format, read_only) *)
| Source_and_ce of string * (Loc.position * color) list * Loc.position option * Env.fformat
(* Source interleaved with counterexamples: contents, list color loc,
loc of the goal, format of the source *)
| Ident_notif_loc of Loc.position
(* Answer the position where an ident is defined *)
type ide_request =
| Command_req of node_ID * string
......@@ -124,6 +126,7 @@ type ide_request =
| Copy_paste of node_ID * node_ID
| Save_file_req of string * string
| Get_first_unproven_node of node_ID
| Find_ident_req of string * string list * string * string
| Unfocus_req
| Save_req
| Reload_req
......@@ -148,6 +151,7 @@ let print_request fmt r =
Whyconf.print_prover_upgrade_policy p2
| Get_file_contents _f -> fprintf fmt "get file contents"
| Get_first_unproven_node _nid -> fprintf fmt "get first unproven node"
| Find_ident_req (_, _, _, _) -> fprintf fmt "find ident"
| Get_task(nid,b,loc) -> fprintf fmt "get task(%d,%b,%b)" nid b loc
| Remove_subtree _nid -> fprintf fmt "remove subtree"
| Copy_paste _ -> fprintf fmt "copy paste"
......@@ -209,8 +213,10 @@ let print_notify fmt n =
| Message msg ->
print_msg fmt msg
| Dead s -> fprintf fmt "dead :%s" s
| File_contents (f, _s, _) -> fprintf fmt "file contents %s" f
| File_contents (f, _s, _, _) -> fprintf fmt "file contents %s" f
| Source_and_ce (_, _list_loc, _gl, _) -> fprintf fmt "source and ce"
| Task (ni, _s, list_loc, _g_loc, _lang) ->
fprintf fmt "task for node_ID %d which contains a list of %d locations"
ni (List.length list_loc) (* print_list_loc list_loc *)
| Ident_notif_loc loc ->
fprintf fmt "ident notification %a" Pretty.print_loc loc
......@@ -117,11 +117,13 @@ type notification =
- [goal_loc] the location of the goal,
- [lang] the language to load in Why3ide for syntax coloring
*)
| File_contents of string * string * Env.fformat
(** File_contents (filename, contents, format) *)
| File_contents of string * string * Env.fformat * bool
(** File_contents (filename, contents, format, read_only) *)
| Source_and_ce of string * (Loc.position * color) list * Loc.position option * Env.fformat
(** Source interleaved with counterexamples: contents and list color loc,
loc of the goal, format of the source *)
| Ident_notif_loc of Loc.position
(** Answer the position where an ident is defined *)
type ide_request =
| Command_req of node_ID * string
......@@ -142,6 +144,8 @@ type ide_request =
| Save_file_req of string * string
(** [Save_file_req(filename, content_of_file)] saves the file *)
| Get_first_unproven_node of node_ID
| Find_ident_req of string * string list * string * string
(** [Find_ident_req (filename, qualification, encapsulating_module, ident] *)
| Unfocus_req
| Save_req
| Reload_req
......
......@@ -547,6 +547,7 @@ let get_modified_node n =
| Task (nid, _, _, _, _) -> Some nid
| File_contents _ -> None
| Source_and_ce _ -> None
| Ident_notif_loc _ -> None
type focus =
......@@ -602,7 +603,7 @@ end
(* File input/output *)
(*********************)
let read_and_send f file_format =
let read_and_send ~read_only f file_format =
try
let d = get_server_data() in
if d.send_source then
......@@ -611,7 +612,7 @@ end
(Session_itp.get_dir d.cont.controller_session) f in
*)
let s = Sysutil.file_contents f in
P.notify (File_contents (f, s, file_format))
P.notify (File_contents (f, s, file_format, read_only))
with Invalid_argument s ->
P.notify (Message (Error s))
......@@ -880,7 +881,7 @@ end
let d = get_server_data () in
let ses = d.cont.controller_session in
let on_file f =
read_and_send (Session_itp.system_path ses f)
read_and_send ~read_only:false (Session_itp.system_path ses f)
(Session_itp.file_format f)
in
iter_on_files ~on_file ~on_subtree:create_node
......@@ -1045,7 +1046,8 @@ end
let l = add_file cont f in
let file = find_file_from_path cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (Session_itp.system_path cont.controller_session file)
read_and_send ~read_only:false
(Session_itp.system_path cont.controller_session file)
(Session_itp.file_format file);
begin
match l with
......@@ -1383,7 +1385,8 @@ end
let read_and_send_files s =
let fs = Session_itp.get_files s in
Hfile.iter (fun _ f ->
read_and_send (Session_itp.system_path s f) (Session_itp.file_format f))
read_and_send ~read_only:false (Session_itp.system_path s f)
(Session_itp.file_format f))
fs
let notify_parsing_errors l =
......@@ -1509,7 +1512,7 @@ end
| Get_file_contents _ | Save_file_req _
| Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req
| Reset_proofs_req -> true
| Reset_proofs_req | Find_ident_req _ -> true
| Get_first_unproven_node ni ->
Hint.mem model_any ni
| Remove_subtree nid ->
......@@ -1524,6 +1527,86 @@ end
else
true
(* Sends a notification of a location together with the file in which this
location appear. (TODO: TBI only send the file if it is not in the
session) *)
let notify_loc loc =
let (f, _, _, _) = Loc.get loc in
let s = Sysutil.file_contents f in
let format = Env.get_format f in
P.notify (File_contents (f, s, format, true));
P.notify (Ident_notif_loc loc)
let find_id_ns (ns_logic: Theory.namespace) (ns_prog: Pmodule.namespace) qs =
Pmodule.(Theory.(
begin match ns_find_ls ns_logic qs with
| ls -> ls.Term.ls_name
| exception Not_found ->
begin match ns_find_pr ns_logic qs with
| pr -> pr.Decl.pr_name
| exception Not_found ->
begin match ns_find_ts ns_logic qs with
| ty -> ty.Ty.ts_name
| exception Not_found ->
begin match ns_find_pv ns_prog qs with
| pv -> pv.Ity.pv_vs.Term.vs_name
| exception Not_found ->
begin match ns_find_its ns_prog qs with
| ity -> ity.Ity.its_ts.Ty.ts_name
| exception Not_found ->
begin match ns_find_xs ns_prog qs with
| xs -> xs.Ity.xs_name
| exception Not_found ->
begin match ns_find_rs ns_prog qs with
| rs -> rs.Expr.rs_name
end
end
end
end
end
end
end))
let find_ident d qualif (encaps_module: string) (f:string) (id: string) =
try
let (r, _) = Env.read_file Pmodule.mlw_language d.controller_env f in
let pmod = Mstr.find encaps_module r in
let ns_prog = pmod.Pmodule.mod_export in
let ns_logic = pmod.Pmodule.mod_theory.Theory.th_export in
let found_id = find_id_ns ns_logic ns_prog (qualif @ [id]) in
let treat_ident found_id =
match found_id.Ident.id_loc with
| None -> P.notify (Message (Error "No location found on ident"))
| Some loc ->
notify_loc loc in
treat_ident found_id
with Not_found -> P.notify (Message (Error "Ident not found"))
(* Locate a string in the task *)
let locate_id d (id: string) nid =
let any = any_from_node_ID nid in
let ses = d.cont.Controller_itp.controller_session in
let locate_in_goal nid =
let _,table = Session_itp.get_task_name_table ses nid in
begin match locate_id d.cont table [id] with
| None -> P.notify (Message (Error "No location found"))
| exception Server_utils.Undefined_id _ ->
P.notify (Message (Error "No location found"))
| Some loc -> notify_loc loc
end in
match any with
| None -> P.notify (Message (Error "Please select a node id"));
| Some (APn nid) ->
locate_in_goal nid
| Some (APa nid) ->
let nid = Session_itp.get_proof_attempt_parent ses nid in
locate_in_goal nid
| Some (ATn nid) ->
let nid = Session_itp.get_trans_parent ses nid in
locate_in_goal nid
| Some (AFile _) | Some (ATh _) ->
P.notify (Message (Error "Please select a goal id"))
(* ----------------- treat_request -------------------- *)
let treat_request d r =
......@@ -1538,7 +1621,9 @@ end
reload_session ();
session_needs_saving := true
| Get_first_unproven_node ni ->
notify_first_unproven_node d ni
notify_first_unproven_node d ni
| Find_ident_req (f, qualif, encaps_module, s) ->
find_ident d.cont qualif encaps_module f s
| Remove_subtree nid ->
remove_node nid;
session_needs_saving := true
......@@ -1568,7 +1653,7 @@ end
let file = Session_itp.find_file_from_path ses
(Sysutil.system_independent_path_of_file f) in
let file_format = Session_itp.file_format file in
read_and_send f file_format
read_and_send ~read_only:false f file_format
| Save_file_req (name, text) ->
save_file name text
| Check_need_saving_req ->
......@@ -1595,6 +1680,8 @@ end
| Strategies st ->
run_strategy_on_task nid st;
session_needs_saving := true
| Locate id ->
locate_id d id nid
| Edit p ->
schedule_edition nid p;
session_needs_saving := true
......
......@@ -143,6 +143,7 @@ let convert_notification_constructor n =
| Task _ -> String "Task"
| File_contents _ -> String "File_contents"
| Source_and_ce _ -> String "Source_and_ce"
| Ident_notif_loc _ -> String "Ident_notif_loc"
let convert_node_type_string nt =
match nt with
......@@ -168,6 +169,7 @@ let convert_request_constructor (r: ide_request) =
| Remove_subtree _ -> String "Remove_subtree"
| Copy_paste _ -> String "Copy_paste"
| Get_first_unproven_node _ -> String "Get_first_unproven_node"
| Find_ident_req _ -> String "Find_ident_req"
| Unfocus_req -> String "Unfocus_req"
| Save_req -> String "Save_req"
| Check_need_saving_req -> String "Check_need_saving_req"
......@@ -214,6 +216,12 @@ let print_request_to_json (r: ide_request): Json_base.json =
| Get_file_contents s ->
convert_record ["ide_request", cc r;
"file", String s]
| Find_ident_req (f, qualif, m, s) ->
convert_record ["ide_request", cc r;
"file", String f;
"qualif", List (List.map (fun x -> String x) qualif);
"module", String m;
"ident", String s]
| Remove_subtree n ->
convert_record ["ide_request", cc r;
"node_ID", Int n]
......@@ -428,11 +436,12 @@ let print_notification_to_json (n: notification): json =
"goal_loc", convert_option_loc goal_loc;
"lang", String lang;
]
| File_contents (f, s, f_format) ->
| File_contents (f, s, f_format, read_only) ->
convert_record ["notification", cc n;
"file", String f;
"content", String s;
"file_format", String f_format;
"read_only", Bool read_only;
]
| Source_and_ce (s, list_loc, goal_loc, f_format) ->
convert_record ["notification", cc n;
......@@ -440,7 +449,11 @@ let print_notification_to_json (n: notification): json =
"loc_list", convert_list_loc list_loc;
"goal_loc", convert_option_loc goal_loc;
"file_format", String f_format
])
]
| Ident_notif_loc loc ->
convert_record ["notification", cc n;
"ident_loc", convert_loc loc]
)
let print_notification fmt (n: notification) =
Format.fprintf fmt "%a" print_json (print_notification_to_json n)
......@@ -510,6 +523,12 @@ let parse_request (constr: string) j =
| _ -> raise (NotRequest "")
end
| "Find_ident_req" ->
let file = get_string (get_field j "file") in
let ident = get_string (get_field j "ident") in
let qualif = List.map get_string (get_list (get_field j "qualif")) in
let m = get_string (get_field j "module") in
Find_ident_req (file, qualif, m, ident)
| "Get_task" ->
let n = get_int (get_field j "node_ID") in
......@@ -812,7 +831,8 @@ let parse_notification constr j =
let f = get_string (get_field j "file") in
let s = get_string (get_field j "content") in
let f_format = get_string (get_field j "file_format") in
File_contents(f,s, f_format)
let read_only = get_bool (get_field j "read_only") in
File_contents(f,s, f_format, read_only)
| "Source_and_ce" ->
let s = get_string (get_field j "content") in
......@@ -821,6 +841,9 @@ let parse_notification constr j =
let f_format = get_string (get_field j "file_format") in
Source_and_ce(s, parse_list_loc l, parse_opt_loc gl, f_format)
| "Ident_notif_loc" ->
let loc = parse_loc (get_field j "ident_loc") in
Ident_notif_loc loc
| s -> raise (NotNotification ("<from parse_notification> " ^ s))
......
......@@ -160,8 +160,8 @@ let print_id s tables =
(* Different constructs are printed differently *)
match d.Decl.d_node, table_id with
| Decl.Dind (_, il), Args_wrapper.Tsprsymbol pr ->
print_constr_string ~print_term:P.print_term ~print_pr:P.print_pr il pr
| _ -> Pp.string_of P.print_decl d
(d, print_constr_string ~print_term:P.print_term ~print_pr:P.print_pr il pr)
| _ -> (d, Pp.string_of P.print_decl d)
(* searching ids in declarations *)
......@@ -230,9 +230,16 @@ let search ~search_both s tables =
let module P = (val Pretty.create pr apr pr pr false) in
Pp.string_of (Pp.print_list Pp.newline2 P.print_decl) l
let locate_id _cont task args =
match args with
| [s] -> let (d, _) = print_id s task in
let id = Ident.Sid.choose d.Decl.d_news in
id.Ident.id_loc
| _ -> raise Number_of_arguments
let print_id _cont task args =
match args with
| [s] -> print_id s task
| [s] -> let (_, s) = print_id s task in s
| _ -> raise Number_of_arguments
let search_id ~search_both _cont task args =
......@@ -244,7 +251,6 @@ type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
let help_on_queries fmt commands =
let l = Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
let l = List.sort sort_pair l in
......@@ -352,6 +358,7 @@ type command =
| Mark_Obsolete
| Focus_req
| Unfocus_req
| Locate of string
| Help_message of string
| Query of string
| QError of string
......@@ -443,6 +450,11 @@ let interp commands_table cont id s =
| Some _ -> Strategies cmd
else
match cmd, args with
| "locate", args ->
begin match args with
| [id] -> Locate id
| _ -> QError "locate expects only one argument"
end
| "edit", _ ->
begin
match id with
......
......@@ -41,6 +41,7 @@ type query =
(* The first argument is not used: these functions are supposed to be given to a
Qtask. *)
val print_id: 'a -> Trans.naming_table -> string list -> string
val locate_id: 'a -> Trans.naming_table -> string list -> Loc.position option
val search_id: search_both:bool -> 'a -> Trans.naming_table -> string list -> string
val list_strategies: Controller_itp.controller -> (string * string) list
......@@ -67,6 +68,7 @@ type command =
| Mark_Obsolete
| Focus_req
| Unfocus_req
| Locate of string
| Help_message of string
| Query of string
| QError of string
......
......@@ -299,6 +299,8 @@ let treat_notification fmt n =
add_new_node fmt id pid typ name detached
| Remove _id -> (* TODO *)
fprintf fmt "got a Remove notification not yet supported@."
| Ident_notif_loc _loc ->
fprintf fmt "Ident_notif_loc notification not yet supported@."
| Initialized _g_info ->
(* TODO *)
fprintf fmt "Initialized@."
......@@ -306,12 +308,12 @@ let treat_notification fmt n =
fprintf fmt "Session is saved@."
| Saving_needed _b -> (* TODO *)
fprintf fmt "got a Saving_needed notification not yet supported@."
| Message (msg) -> treat_message_notification fmt msg
| Message msg -> treat_message_notification fmt msg
| Dead s ->
fprintf fmt "Dead notification: %s\nExiting.@." s;
(* This exception is matched in Unix_Scheduler *)
raise Exit
| File_contents (f, s, _) ->
| File_contents (f, s, _, _) ->
fprintf fmt "File %s is:\n%s" f s (* TODO print this correctly *)
| Source_and_ce _ ->
fprintf fmt "got a Source_and_ce notification not yet supported@." (* TODO *)
......
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