Petanque_shell.Protocol_shellSourcemodule Lsp = Fleche_lspset_workspace { debug; root } sets the current workspace to the directory specified in root
toc { uri } returns the table of contents for a document; the semantics are quite Coq-specific, in particular, each sentence of the document can contribute