aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* 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.
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
|
* Fixing bug #3858 and #3817 in one stroke.Gravatar Pierre-Marie Pédrot2014-12-14
|
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Better commentGravatar Enrico Tassi2014-12-01
|
* Future: API for blocking futuresGravatar Enrico Tassi2014-11-28
|
* better to always print the thread idGravatar Enrico Tassi2014-11-27
|
* async_queries_* merged with async_proofs_*Gravatar Enrico Tassi2014-11-27
|
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
|
* Making map_union a standard function of the ML library.Gravatar Hugo Herbelin2014-11-19
|
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Removing deprecated code handling color in Pp.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Adding a terminal library.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Move conjugate_verb_to_be next to cString.plural.Gravatar Hugo Herbelin2014-11-13
|
* 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/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
| | | | | | printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
* lib/richPp: Fix a bug related to the compatibility with ocaml 3.12Gravatar Yann Régis-Gianas2014-11-05
| | | | | | | - The previous version of this module was using a feature of the Format module of ocaml 4.01. - Add comments.
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/richPp: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
| | | | | A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it.
* lib/Xml_parser.parse: Publish and document new interface.Gravatar Regis-Gianas2014-11-04
|
* lib/Xml_printer.pcdata_to_string: Publish.Gravatar Regis-Gianas2014-11-04
|
* printing/RichPrinter: New API for rich pretty-printing.Gravatar Regis-Gianas2014-11-04
| | | | | printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping.
* lib/Pp.rewrite: New.Gravatar Regis-Gianas2014-11-04
| | | | | Allow strings of a pretty-print to be rewritten just before the actual output.
* lib/Xml_printer: Handle non-breakable spaces.Gravatar Regis-Gianas2014-11-04
|
* lib/Xml_parser.parse: Make canonicalization optional. (By default, it is ↵Gravatar Regis-Gianas2014-11-04
| | | | applied, to preserve previous behaviors.
* lib/Xml_parser: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/Xml_parser: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Xml_lexer: Handle non-breakable spaces.Gravatar Regis-Gianas2014-11-04
|
* RichPp: New module.Gravatar Regis-Gianas2014-11-04
| | | | | | | | | It is responsible for turning a tagged pretty-printing into a semi-structured document. clib.mllib: Include RichPp as well as Xml_*. The migration of Xml_* from lib to clib is needed by RichPp depends on these modules.
* Xml_datatype.gxml: New type for semi-structured documents.Gravatar Regis-Gianas2014-11-04
| | | | Xml_parser, Xml_printer: Use it.
* lib/Pp: Publish combinators for tags opening and closing.Gravatar Regis-Gianas2014-11-04
|
* lib/Pp.ppcmd_token:Gravatar Regis-Gianas2014-11-04
| | | | | | | 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.
* lib/Pp: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Add an [Info Level] option to print info traces automatically.Gravatar Arnaud Spiwack2014-11-01
| | | | [Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
* 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: new worker for queriesGravatar Enrico Tassi2014-10-31
| | | | | | | | | | | | | | | | | | | | | | | | With the options -async-queries-always-delegate queries are always delegated to a worker process (Eval, Check, ...). Users of PIDE based UIs (in Denmark) reported that the current behavior of processing query synchronously is rather unexpected when one is used to get proofs processed asynchronously. Non instantaneous queries are part of many scripts and are there as "tests" for testing the execution of recursive functions. A standard proof script shape in an ongoing work by Appel and Bengtson is made of blocks like: - recursive function definition, - some tests, - some proofs And one cannot quickly jump over the tests (only the proofs). Enclosing the queries into dummy proofs to recover a reactive UI is just annoying. Hence this patch. Currently CoqIDE is not able to integrate the asynchronous feedback of the query workers into the document, hence if one passes the option to CoqIDE one only gets a boolean out of queries (processed/error).
* Changed implementation of lib/heap.ml to use Braun treesGravatar Jean-Christophe Filliatre2014-10-25
| | | | | | | | The previous implementation was embarrassingly naive and inefficient. For elements with the same priority, this new implementation may return a maximum element that is different (yet still with the highest priority, of course). This code is used only in tactic firstorder.
* -help failing (fix 3762)Gravatar Enrico Tassi2014-10-24
|
* Monad: change the error managing of two-list combinators.Gravatar Arnaud Spiwack2014-10-23
| | | Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
| | | | | | | | | | Goal printing was partially broken. Some commands in vernacentries were printing, but not all of them. Moreover an unlucky combination of `Flags.verbosely (fun () -> interp "Set Silent")` was making the silent flag not settable anymore. Now STM always print the open goals after a command when run in interactive mode via coqtop or emacs. More modern GUI do ask for the goals.
* An additional [List.iter] monadic combinator.Gravatar Arnaud Spiwack2014-10-22
|
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
| | | | For optimisation purposes.
* Proofview: move [list_goto] to the [CList] module.Gravatar Arnaud Spiwack2014-10-22
| | | | It is, after all, a generic function about lists.
* Add a two-list monadic fold_left iterator.Gravatar Arnaud Spiwack2014-10-22
|
* Small optimisation in the monadic list combinators.Gravatar Arnaud Spiwack2014-10-22
| | | | The monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold.
* Factor module signatures.Gravatar Arnaud Spiwack2014-10-22
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-21 18:11:23 +0000