diff options
| author | Emilio Jesus Gallego Arias | 2018-11-08 20:52:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 00:33:31 +0100 |
| commit | d5aaa0ff95ce811dbca6644dad8bde70f7739514 (patch) | |
| tree | ca1e7306263ff242832f97a4df929ba15ceab2aa /kernel/indtypes.ml | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
[topfmt] Add phase attribute for toplevel printing.
This is localized version of #8833, but instead of adding a phase
attribute which, as pointed by @gares has some problematic semantics,
we add a local one to the toplevel functions.
This moves the imperative part of the API to a better-delimited scope
and allows to progress with the separation of the interactive and
compilation API.
Note that still quite a few issues do remain in the "Feedback" path,
for example, idetop and other feedback clients cannot get a hold of
the feedback early enough as to direct init messages to the IDE part.
This is for example a serious issue of the API that shall be treated
separately.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions
