coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Encapsulate xml serialization in xmlprotocol.mli	Emilio Jesus Gallego Arias	2016-06-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This eases the task of replacing/improving the serializer, as well as making it more resistant. See pitfalls below: Main changes are: - fold `message` type into `feedback` type - make messages of type `Richpp.richpp` so we are explicit about the content being a rich document. - moved serialization functions for messages and stateid to `Xmlprotocol` - improved a couple of internal API points (`is_message`). Tested.
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Rich printing of messages.	Pierre-Marie Pédrot	2015-09-20
\|/
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Feedback: API cleaned up, documented and made user extensible	Enrico Tassi	2014-11-27
\|
*	Feedback message: hold extra info to help routing	Enrico Tassi	2014-10-31
\| \| \| \| \|	PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel
*	When loading libraries, feed back dependencies.	Carst Tankink	2014-10-13
\| \| \| \| \| \| \| \|	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.
*	STM: report the (structured) goals as XML	Carst Tankink	2014-10-01
\| \| \| \| \|	The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
*	STM: code restructured to reuse task queue for tactics	Enrico Tassi	2014-08-05
\|
*	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink	2014-08-04
\|
*	Feedback: LoadedFile + Goals	Enrico Tassi	2014-07-11
\| \| \| \| \|	LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
	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/