URI interface for pre-highlighting parts of the graph.

[kohlhase]

We should extend the URI interface, so that we can pre-highlight parts of the graph, e.g. theories by name. I am imagining something like

https://mmt.mathhub.info/graphs/tgview.html?type=archivegraph&graphdata=smglom/arithmetics&highlight=realpns,realplns.de,realpns.en

where the names behind the highlight parameter will be highlighted (i.e. made red or so). This is the highlighting I thought of in #24.

[Shadow992]

Maybe we should not explicitly model this in the URI, but combine it with our idea of saving a "shareable snapshot" of the current graph. However this will in first place be shared by URI, too.

Edit:
We could start with this as I realised we also need this generated by server.

[Shadow992]

Implemented with 370ea36

Example usage:

http://neuralocean.de/graph/theorygraph.php?uri=http://neuralocean.de/graph/test/pvs.json&highlight=identity*,extend

"*" can be used anywhere as wildcard
"," separates different node names to highlight

[kohlhase]

very nice. Do not forget to document.

[freifrauvonbleifrei]

Neat! :)