# This file adds support for bookmarks in GPS # Missing in this very partial implementation: # - Add known bookmarks to a menu dynamically, for easy jumps # This is mostly reimplemented in GPS itself at this point import GPS GPS.Editor.register_highlighting("bookmarks", "orange", True) def add_bookmark(): context = GPS.current_context() if isinstance(context, GPS.FileContext): name = GPS.MDI.input_dialog("Name of bookmark", "Name") if name != (): GPS.Locations.add("Bookmarks", context.file(), GPS.Editor.cursor_get_line( context.file().name()), GPS.Editor.cursor_get_column( context.file().name()), name[0], "bookmarks") GPS.parse_xml(""" Add a bookmark for the current line bookmarks.add_bookmark() Navigate/Bookmarks Add bookmark """)