old RESTful interface

• GET /dir/dir. List folder dir from repository. Returns a list of filenames for use with graph
• GET /hets-lib/file?format. Get the development graph of file file. Returns the graph as svg, xml or dot (depending on format), where all nodes and edges have been annotated with their ids. (Also class names or other information needs to be added to SVG). A special format is also "session" that is just a number to access the graph later.
• GET /libraries/coded-iri/development_graph?format=f. Two output formats: (1) just list of nodes and links with their IRIs, (2) whole DG. For now, the interface is synchronous; later on, also an asynchronous answer may be given "please call later". There is no session id. The DG contains IRIs for the individual specs and symbols. for HetCASL, the IRI is library-iri?spec-name resp. library-iri?spec-name?symbol-name. For DOL, IRIs are determined by DOL's prefixing mechanism. Optionally, rettrieve DG for a specific session
• POST /libraries/coded-iri/sessions create a new proof session for development graph of coded-iri, like current GET command, answer: 201 and location header (=path on server) including the session id.
• GET /sessions/id?format=f get proof state of session id as a DG
• efficiency: Hets is provided with caching option, namely one caching location in the file system. The file system should be used as a cache for IRIs, e.g. path-to-cache/sha256sum-of-iri. Clients of Hets should use the same caching mechanism.
• GET /menus. Get menu structure. Returns a list of triples (XQuery, displayname, action). Actions are node, theory, edge, proveform... and correspond to actions in the Hets development graph menus, and also to actions in this interface. Generally, these should be actions of type GET file?action_name&id=id, that is, the parameters are always the current file and the current (node or edge) id. XQuery can also be "" to denote a global action or "/" to be a menu entry global to the current development graph.
• GET /nodes/coded-iri?library=coded-iri&session=id. Returns info for the node coded-iri (corresponds to show node info). Optionally, a library where the node resides and a proof session can be specified.
• GET /nodes/coded-iri/theory?library=coded-iri&session=id. Returns theory (for now as ASCII text) of the node coded-iri (corresponds to show theory).
• GET /edges/coded-iri?library=coded-iri&session=id. Returns info for the edge coded-iri (corresponds to show edge info).

The development graph calculus interface (stateful with sessions)

• PUT /libraries/coded-iri/proofs/id/command execute command for session id
• PUT /sessions/id/command?node=iri&edge=iri. Call command on session id, e.g. applying a development graph calculus rule. Returns a success/failure state. (A returned session id is unchanged.). Only one of node and edge may be provided.
• GET /sessions/id/provers?node=iri&translation=iri. Get provers for the node iri (or all nodes' provers, if no iri is given). If translation is given, give those provers available after translation.
• GET /sessions/id/translations?node=iri. Get comorphisms for the node iri (or all nodes' translations, if no iri is given)
• PUT /sessions/id/prove?node=iri?prover=name&translation=iri&timeout=secs&include=true. Call the given prover (or the first one if not given) on the given node (or all nodes, if non is given) using the given (or first) comorphism and the other optional parameters. Previously proven theorems are not included by default as axioms, unless include=true is specified.