Mentions légales du service

Skip to content
  • Sylvain Dailler's avatar
    Ide/itp_server: experimental ctrl-C ctrl-L (àla merlin) · 0e25deba
    Sylvain Dailler authored
    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