aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.mli
Commit message (Collapse)AuthorAge
* Improving spacing in printing disjunctive patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | Adding a space before the bar separating disjunctive patterns. Removing an extra space after the bar for inner disjunctive patterns.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* completing a sentence in a commentGravatar Matej Košík2017-06-07
|
* [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
* [pp] Hide the internal representation of `std_ppcmds`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | Following a suggestion by @ppedrot in #390, we require `Pp` clients to be aware that they are using a "view" on the `std_ppcmds` type. This is not extremely useful as people caring about the documents will indeed have to follow changes in the view, but it costs little to play on the safe side here for now. We also introduce a more standard notation, `Pp.t` for the main type.
* [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics.
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`.
* [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | For legacy reasons, pretty printing required to provide a "tag" interpretation function `pp_tag`. However such function was not of much use as the backends (richpp and terminal) hooked at the `Format.tag` level. We thus remove this unused indirection layer and annotate expressions with their `Format` tags. This is a step towards moving the last bit of terminal code out of the core system.
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent.
* [pp] Remove redundant white spacing pp construct.Gravatar Emilio Jesus Gallego Arias2017-03-21
|
* [pp] Force well-formed boxes by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | We replace open/close box commands in favor of the create box ones.
* [pp] Force well-tagged docs by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | We replace open/close tag commands by a well-balanced "tag" wrapper.
* [pp] Implement n-ary glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
|
* [pp] Make pp public to allow serialization.Gravatar Emilio Jesus Gallego Arias2017-03-21
|
* [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
* [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | Mostly unused, we ought to limit spacing in the boxes themselves.
* [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags.
* Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
|\
* \ Merge PR #224 into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \
* | | Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | done by the Ppcmd_comment token) and so that lexing/parsing side-effects are collected at the same place, i.e. in CLexer.
| * | [pp] Remove duplicate color logger.Gravatar Emilio Jesus Gallego Arias2016-09-30
|/ / | | | | | | | | | | | | | | | | | | | | We use the same printing path for color and mono terminal output, thus removing the duplicate printers which avoids problems as they don't have to be kept in sync anymore. We tag unconditionally but set the `pp_tag` tagger properly. This removes IO from `Ppstyle` with IMO is the right thing to do. Test suite passes.
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | Add documentation to the low-level `Pp` functions.Gravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | Thanks to HH for pointing it out.
| * Remove tabulation support from pretty-printing.Gravatar Guillaume Melquiond2016-06-02
|/ | | | | | | | This mechanism relied on functions that are deprecated in recent versions of ocaml. It was incorrectly used for the most part anyway. The only place that was using tabulations correctly is "print_loadpath", so there is a minor regression there: physical paths of short logical paths are no longer aligned.
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-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'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * typoGravatar Enrico Tassi2016-05-04
| |
* | In pr_clauses, do not print a leading space by default so that it canGravatar Hugo Herbelin2016-04-09
| | | | | | | | | | | | | | be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
|/
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
| | | | | | | The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
* Removing dead code in Pp.Gravatar Pierre-Marie Pédrot2015-04-23
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
| | | | | Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
| | | | | Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message.
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
|
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
|
* Adding a dynamic tag type in Pp.Gravatar Pierre-Marie Pédrot2014-11-10
|
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
| | | | | A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it.
* lib/Pp.rewrite: New.Gravatar Regis-Gianas2014-11-04
| | | | | Allow strings of a pretty-print to be rewritten just before the actual output.
* lib/Pp: Publish combinators for tags opening and closing.Gravatar Regis-Gianas2014-11-04
|
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
| | | | | PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
|
* make the standard logging facility stm awareGravatar Enrico Tassi2014-07-11
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-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/
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Coqide ported to STMGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7