{
  "title": "Document Search",
  "description": "Document search plugin.",
  "jupyter.lab.setting-icon": "ui-components:search",
  "jupyter.lab.setting-icon-label": "Document Search",
  "jupyter.lab.menus": {
    "main": [
      {
        "id": "jp-mainmenu-edit",
        "items": [
          {
            "type": "separator",
            "rank": 10
          },
          {
            "command": "documentsearch:start",
            "rank": 10
          },
          {
            "command": "documentsearch:highlightNext",
            "rank": 10
          },
          {
            "command": "documentsearch:highlightPrevious",
            "rank": 10
          },
          {
            "type": "separator",
            "rank": 10
          }
        ]
      }
    ]
  },
  "jupyter.lab.shortcuts": [
    {
      "command": "documentsearch:start",
      "keys": ["Accel F"],
      "selector": ".jp-mod-searchable"
    },
    {
      "command": "documentsearch:highlightNext",
      "keys": ["Accel G"],
      "selector": ".jp-mod-searchable"
    },
    {
      "command": "documentsearch:highlightPrevious",
      "keys": ["Accel Shift G"],
      "selector": ".jp-mod-searchable"
    },
    {
      "command": "documentsearch:end",
      "keys": ["Escape"],
      "selector": ".jp-mod-searchable"
    }
  ],
  "properties": {
    "searchDebounceTime": {
      "title": "Search debounce time (ms)",
      "description": "The debounce time in milliseconds applied to the search input field. The already opened input files will not be updated if you change that value",
      "type": "number",
      "default": 500,
      "minimum": 0
    }
  },
  "additionalProperties": false,
  "type": "object"
}
