aboutsummaryrefslogtreecommitdiff
path: root/lib/pp.ml
AgeCommit message (Collapse)Author
2015-10-02emacs output mode: Added <infomsg> tag to debug messages.Pierre Courtieu
So that they display in response buffer.
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
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.
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
2015-04-23Removing dead code in Pp.Pierre-Marie Pédrot
2015-04-22Pp: obsolete comment.Arnaud Spiwack
Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
2015-04-22Do not use list concatenation when gluing streams together, just mark them ↵Guillaume Melquiond
as glued. Possible improvement: rotate using the left children in the glue function, so that the iter function becomes mostly tail-recursive. Drawback: two allocations per glue instead of a single one. This commit makes the following command go from 7.9s to 3.0s: coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
2015-02-26Fixing printing of ordinals.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
I added a emacs_logger. Still need to cleanup std_logger.
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
2014-12-15Changed bullet informations to warning for better display in PG.Pierre Courtieu
Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message.
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-11-15Removing deprecated code handling color in Pp.Pierre-Marie Pédrot
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-10Adding a dynamic tag type in Pp.Pierre-Marie Pédrot
2014-11-04lib/Pp.tag: New.Regis-Gianas
A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it.
2014-11-04lib/Pp.rewrite: New.Regis-Gianas
Allow strings of a pretty-print to be rewritten just before the actual output.
2014-11-04lib/Pp: Publish combinators for tags opening and closing.Regis-Gianas
2014-11-04lib/Pp.ppcmd_token:Regis-Gianas
Extend this type with Ppcmd_open_tag and Ppcmd_close_tag. lib/Pp.ppcmd_pp_dirs: Handle these tags with a straightforward translation to corresponding Format commands.
2014-11-04lib/Pp: Cosmetics.Regis-Gianas
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-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-07-29Pp: only one default feedback idEnrico Tassi
2014-07-11make the standard logging facility stm awareEnrico Tassi
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/
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2013-11-08Do not compute formatter UTF8 length at creation time.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17069 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Some more hand-written comparison functions to avoid polymorphic comparison.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Coqide ported to STMgareuselesinge
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
2013-05-23Fixing #3042ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16530 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-16Fixing Pp.strbrk which was reversing words.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16529 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-16std_ppcmds is persistent, errors can be printed twicegareuselesinge
The patch is very simple and naive, there is no lazy involved. This makes a difference only for strbrk. An extra patch may be necessary if there is a noticeable slowdown. In any case the data type used is opaque, to ease any future optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16528 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
exception information addition facility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Actually adding backtrace handling.ppedrot
I hope I did not forget some [with] clauses. Otherwise, some stack frame will be missing from the debug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Removed a unused function in Ppppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16048 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14lib/Pp:regisgia
Backtrack on the removal of a type definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15799 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15795 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-10Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5ppedrot
anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15792 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19reparation du make depend et du .dependletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:43:27 +0000