Commit c3f2a908 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'improve_ctrll' into 'master'

Improve ctrll

See merge request !247
parents 11b0ea10 f732b316
......@@ -23,6 +23,10 @@ external reset_gc : unit -> unit = "ml_reset_gc"
let debug = Debug.lookup_flag "ide_info"
let debug_stack_trace = Debug.lookup_flag "stack_trace"
let () =
(* Allow global locations to be saved for Find_ident_req *)
Debug.set_flag Glob.flag
(***************************)
(* Debugging Json protocol *)
(***************************)
......@@ -2077,12 +2081,12 @@ let get_word_around_iter iter =
let start_iter = get_left_words iter in
let end_iter = get_right_words iter in
let text = start_iter#get_text ~stop:end_iter in
(start_iter, text)
(start_iter, text, end_iter)
(* This function check for immediate quantification (not for scope yet) *)
let rec get_qualif acc start_iter =
if start_iter#get_text ~stop:start_iter#forward_char = "." then
let (start_iter, text) = get_word_around_iter start_iter#backward_char in
let (start_iter, text, _) = get_word_around_iter start_iter#backward_char in
if Strings.char_is_uppercase
(start_iter#get_text ~stop:start_iter#forward_char).[0] then
get_qualif (text :: acc) start_iter#backward_char
......@@ -2096,7 +2100,7 @@ let get_module (iter: GText.iter) =
| None -> print_message ~kind:1 ~notif_kind:"Error"
"cannot find encapsulating module"; None
| Some (_, end_iter) ->
let (_, text) = get_word_around_iter end_iter#forward_char in
let (_, text, _) = get_word_around_iter end_iter#forward_char in
Some text
(* find_cursor_ident: finds the ident under cursor and scroll to its definition
......@@ -2112,19 +2116,20 @@ let find_cursor_ident, get_back_loc =
try
if file = "Task" then
let iter = view#buffer#get_iter `SEL_BOUND in
let (_, text) = get_word_around_iter iter in
let (_, text, _) = get_word_around_iter iter in
interp ("locate " ^ text)
else
let iter = view#buffer#get_iter `SEL_BOUND in
let (start_iter, text) = get_word_around_iter iter in
let (start_iter, text, end_iter) = get_word_around_iter iter in
if text = "" then
()
else
let qualif = get_qualif [] start_iter#backward_char in
match get_module start_iter with
| Some enc_module ->
send_request (Find_ident_req (file, qualif, enc_module, text))
| None -> ()
let l = start_iter#line + 1 in
let b = start_iter#line_offset in
let e = end_iter#line_offset in
let f = file in
let loc = Loc.user_position f l b e in
send_request (Find_ident_req loc)
with SearchLimit ->
print_message ~notif_kind:"Ide_error" ~kind:1
"Search limit overflow: the word is too long"
......
......@@ -18,14 +18,18 @@ let () = Debug.unset_flag flag (* make sure it is unset by default *)
type def_use = Def | Use
let glob = Hashtbl.create 5003
(* could be improved with nested hash tables *)
let glob = Hashtbl.create 16
(* Hash [file -> Hash [(line, column) -> ident]] *)
let key loc = let f, l, c, _ = Loc.get loc in f, l, c
let key loc = let f, l, c, _ = Loc.get loc in f, (l, c)
let add loc idk =
let k = key loc in
if not (Hashtbl.mem glob k) then Hashtbl.add glob k idk
let kf, k = key loc in
match (Hashtbl.find glob kf) with
| hash_f -> if not (Hashtbl.mem hash_f k) then Hashtbl.add hash_f k idk
| exception Not_found ->
let hash_f = Hashtbl.create 255 in
Hashtbl.add glob kf hash_f
let def ~kind id =
Opt.iter (fun loc -> add loc (id, Def, kind)) id.id_loc
......@@ -33,8 +37,15 @@ let def ~kind id =
let use ~kind loc id =
add loc (id, Use, kind)
let clear f =
match Hashtbl.find glob f with
| exception Not_found -> ()
| hash_f -> Hashtbl.clear hash_f
let find loc =
Hashtbl.find glob (key loc)
let (kf, k) = key loc in
let hash_f = Hashtbl.find glob kf in
Hashtbl.find hash_f k
(* FIXME allow several entries for the same loc, find returns all of them,
and why3doc inserts several anchors *)
......@@ -19,6 +19,9 @@ val def: kind:string -> ident -> unit
val use: kind:string -> Loc.position -> ident -> unit
(** [use loc id] registers that [id] is used at position [loc] *)
val clear: string -> unit
(** [clear file] clears the locations association for said [file] *)
type def_use = Def | Use
val find: Loc.position -> ident * def_use * string
......
......@@ -1581,6 +1581,7 @@ let type_module file env loc path (id,dl) =
file
let type_mlw_file env path filename mlw_file =
if Debug.test_flag Glob.flag then Glob.clear filename;
let file = Mstr.empty in
let loc = Loc.user_position filename 0 0 0 in
let file =
......
......@@ -126,7 +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
| Find_ident_req of Loc.position
| Unfocus_req
| Save_req
| Reload_req
......@@ -151,7 +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"
| 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"
......
......@@ -144,8 +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] *)
| Find_ident_req of Loc.position
(** [Find_ident_req (position)] *)
| Unfocus_req
| Save_req
| Reload_req
......
......@@ -16,6 +16,7 @@ open Controller_itp
open Server_utils
open Itp_communication
(**********************************)
(* list unproven goal and related *)
(**********************************)
......@@ -1537,50 +1538,15 @@ end
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) =
let find_ident (loc: Loc.position) =
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"))
let (id, _, _) = Glob.find loc in
begin match id.Ident.id_loc with
| None -> ()
| Some loc -> notify_loc loc
end
with Not_found ->
P.notify (Message (Error "Ident not found: try saving the file."))
(* Locate a string in the task *)
let locate_id d (id: string) nid =
......@@ -1622,8 +1588,8 @@ end
session_needs_saving := true
| Get_first_unproven_node ni ->
notify_first_unproven_node d ni
| Find_ident_req (f, qualif, encaps_module, s) ->
find_ident d.cont qualif encaps_module f s
| Find_ident_req loc ->
find_ident loc
| Remove_subtree nid ->
remove_node nid;
session_needs_saving := true
......
......@@ -179,6 +179,13 @@ let convert_request_constructor (r: ide_request) =
| Reset_proofs_req -> String "Reset_proofs_req"
| Get_global_infos -> String "Get_global_infos"
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])
open Whyconf
let convert_policy u =
......@@ -216,12 +223,9 @@ 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) ->
| Find_ident_req loc ->
convert_record ["ide_request", cc r;
"file", String f;
"qualif", List (List.map (fun x -> String x) qualif);
"module", String m;
"ident", String s]
"loc", convert_loc loc]
| Remove_subtree n ->
convert_record ["ide_request", cc r;
"node_ID", Int n]
......@@ -257,13 +261,6 @@ 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])
(* Converted to a Json list for simplicity *)
let convert_option_loc (loc: Loc.position option) : Json_base.json =
let l =
......@@ -524,11 +521,8 @@ let parse_request (constr: string) j =
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)
let loc = parse_loc (get_field j "loc") in
Find_ident_req loc
| "Get_task" ->
let n = get_int (get_field j "node_ID") in
......
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