Commit 0e25deba authored by Sylvain's avatar Sylvain Committed by Sylvain Dailler

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

This feature should add a shortcut (ctrl-l) to scroll to the location
definition of the ident under the user cursor. To go back to the first
location ctrl-& should work.

Implementation:
The IDE detects:
- the word under the cursor,
- the possible immediate (only) qualification of this word,
- the module in which this is defined,
- the source file in which this is queried

and sends it in the request Find_ident_req to the server.

The itp server calls the parsing on this file (which should only returns
the already loaded pmodule (the itp_server is running)). We use this
module to first find the right module in which the ident is defined and
then find its definition location.

It then notifies the IDE with both the file (in read_only mode) and the
location in Ident_notif_loc. The IDE adds the file (as read only) and
scroll to the given location.
When in read_only, the file_contents notification does not trigger
regenerating the file because we don't want the user to lose her changes.

Note that the read_only file can be removed with a right click on their
title.

Note also that, when coming from a task, ctrl+l instead calls a
Command_req containing the identifier (and the subsequent Locate command)
because in this case we dont need the result of the source file pmodule to
discover the location.

* src/ide/why3ide.ml
(notebook, task_view, create_source_view): Relocate this after the message
zone in order to be able to use print_message in the source_view
(create_source_view): Remove reference n which was counting source_page.
This is an information we can get when appending a tab. Adding an eventbox
on the tab title labels. Use markup to display the label.
(save_cursor_loc): Now takes the reference we want to save. We use it to
save a location for ctrl-&.
Change default column location from 1 to 0 to avoid crashing the IDE on
lines that contain 0 characters.
(get_word_around_iter): Gets a text_iter and returns the words under this
location together with the iter corresponding to the start of the word.
(get_qualif): Return the qualification of a word: A.B.C.word
(get_module): Return the encapsulating module
(find_cursor_ident): send the request to the server for location of the
ident under the current cursor. (binded to ctrl+l)
(get_back_loc): return to previous location (binded to ctrl+&)
(treat_notification): On File_contents, if the file exists (a priori a
session file), and the file is read_only (comes from ctrl+l), do not
reload the file buffer.
On Ident_notif_loc, just scroll to the given location

* src/session/itp_communication.ml*
Adding Find_ident_req and Ident_notif_loc. Add a read_only boolean to
File_contents notification.

* src/session/itp_server.ml
(traverse_modules, notify_loc, find_ident): Used to locate an identifier
in modules and send the corresponding notification
(locate_id): Used when ctrl+l comes from a task.

* src/session/server_utils.ml
Adding command Locate converted from Command_req("locate", ). The effect
is to scroll to the location of the given ident.
parent f82143b1
......@@ -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
......
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,97 @@ end
else
true
(* This function takes a module and a qualification and it tries to
recover the oldest module (A.B.C.D -> A). *)
let traverse_modules (qualif: string list) pmod =
(* Heuristics to find modules used *)
let find_mod mod_units =
List.fold_left (fun acc mu -> match mu with
| Pmodule.Uuse pm -> Some pm
| Pmodule.Uclone mi -> Some mi.Pmodule.mi_mod
| _ -> acc) None mod_units in
let search_scope mod_units mod_name =
let found_mod = ref None in
List.iter (fun munit ->
match munit with
| Pmodule.Uscope (scope, munit_list) when scope = mod_name ->
found_mod := Some munit_list
| _ -> ()) mod_units;
match !found_mod with
| None -> None
| Some fm -> find_mod fm in
List.fold_left (fun pmod fst_mod ->
let mod_units = pmod.Pmodule.mod_units in
match search_scope mod_units fst_mod with
| None -> pmod (* Fallback on last module when one is not found *)
| Some new_pmod -> new_pmod)
pmod qualif
(* 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_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
(* Find the modules in which ident appear *)
let pmod = traverse_modules qualif pmod in
let mod_known = pmod.Pmodule.mod_known in
let find_ident = ref [] in
let () =
Ident.Mid.iter (fun id' _ -> if id'.Ident.id_string = id then
find_ident := id' :: !find_ident) mod_known 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
(match !find_ident with
| [found_id] ->
treat_ident found_id
| [] ->
let msg = "Ident not found: it may be a local ident" in
P.notify (Message (Error msg))
| _ ->
List.iter treat_ident !find_ident;
let msg = "Several Ident found: location may be imprecise" in
P.notify (Message (Error msg)))
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 +1632,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 +1664,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 +1691,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