Ontohub services

[ebolloff]

• Translate formula along signature morphism (hets)
• Flatten a theory (hets)
• Compute colimit of a network (hets)
• Compute normal form of a structured OMS/graph (hets)
• Syntax highlighting, autocomplete, resolve origin of symbol, correction, includes (hets)
• Show all open proof obligations in OMS graph (hets)
• OMS graph transformation (hets; proof rule, apply comorphism)
• Show and inspect refinement tree (hets)
• Parse OMS (hets)
• Prove proof obligation (hets)
• Parse string in context (hets)

• QMT (hets; parse, check, simplify, infer type, present, map, filter, sparql-like)

• List all unproven theorems of a flat theory
• List all indirect imports of a theory (recursive database)
• GET URI
• POST content
• GET SVG (multiple graphs)
• Search

• Admin commands

• Subterm selection (client side)
• Folding (client side)
• Visibility changes (client side; infered types, redundant brackets, implicit arguments)
• Tooltip (client side)

[phyrog]

I believe we can close this issue for now. If needed, we can copy this to the wiki, which seems to be the better place for this.

Ping @tillmo