| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
Cd can make the relative path of the opened file wrong,
and hence not available anymore when we reopen it to compute
the line number.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The lexer parses bullets only at the beginning of sentence. In
particular, the lexer recognizes sentences (this feature was
introduced for the translator and it is still used for the
beautifier). It recognized "." but not "...'. I added "..." followed
by space or eol as a terminator of sentences. I hope this is
compatible with the rest of the code dealing with end of
sentences.
Fixed also parse_to_dot which was not aware of "...".
Maybe there are similar things to do with coqide or PG?
|
| | |
|
| |
|
|
| |
The removed code isn't used locally and isn't exported in the signature
|
|
|
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
|
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Maxime Dénès
Guillaume Melquiond
Enrico Tassi
Hugo Herbelin
Pierre Letouzey