1. 21 Oct, 2019 1 commit
  2. 17 Oct, 2019 1 commit
  3. 16 Oct, 2019 9 commits
  4. 15 Oct, 2019 2 commits
  5. 11 Oct, 2019 6 commits
  6. 10 Oct, 2019 3 commits
  7. 09 Oct, 2019 4 commits
    • DAILLER Sylvain's avatar
      Merge branch 'ctrl_l' into 'master' · 025c5e94
      DAILLER Sylvain authored
      Ide/itp_server: experimental ctrl-C ctrl-L (àla merlin)
      
      See merge request !242
      025c5e94
    • Sylvain Dailler's avatar
    • Sylvain Dailler's avatar
      why3web: fix why3_js.ml · b36fb788
      Sylvain Dailler authored
      b36fb788
    • Sylvain's avatar
      Ide/itp_server: experimental ctrl-C ctrl-L (àla merlin) · 0e25deba
      Sylvain 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
  8. 08 Oct, 2019 1 commit
  9. 07 Oct, 2019 13 commits