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.0e25deba
To find the state of this project's repository at the time of any of these versions, check out the tags.