aboutsummaryrefslogtreecommitdiff
path: root/lib/feedback.ml
AgeCommit message (Collapse)Author
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel
2014-10-13When loading libraries, feed back dependencies.Carst Tankink
These dependencies between files can be used by UIs to guide compilation and reloading of files. FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar. FileDependency (None, "/bar.v") means the current file depends on bar.
2014-10-01STM: report the (structured) goals as XMLCarst Tankink
The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
2014-06-25all coqide specific files moved into ide/Enrico Tassi
lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/