| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- Removing tag "found" (unused since bd18c0821 "Now CoqIDE has a nice
find & replace mechanism").
- Removing setting the priority of the debugging tag edit_zone: it was
set at exactly the level it would have been by default minus 1,
which is the level of tooltip, which have no associated visible
markers, so the setting was a priori w/o effect.
- For clarity, reorganizing order of tags into ephemere ones and non
ephemere ones.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We change the relative priority of errors and warnings, so that the
error takes precedence.
It is unsure that it is universally the best choice. If the location
of the error is finer than the one of the warning, it is better. In
the other way round, it might be less good, e.g. if understanding the
warning helps to understand the error.
Maybe the best policy would be to test the relative locations of the
warning and error?
Trying to consider the error as more important, at the current time.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|\ |
|
| | |
|
|/
|
|
|
| |
A lot of legacy code has been removed in the process in favour of
signal-based interactions.
|
|
|
|
|
|
|
|
|
|
|
| |
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
#FFCCCC is quite dark on some beamers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
The double underline has some bugs, sometimes the lower line
is not correctly cleared.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This simplifies the whole document business: the document on the Coq
side has the very same nodes as the CoqIDE document, there are no "fake"
nodes in the CoqIDE document to be skipped over.
We keep the comment tag stamped by the coq_lexer module, since we may
want to allow edits in there without telling Coq (as proof general
does). Not implemented yet, but doable thanks to the comment tag.
Pierre Boutillier suggested that this makes back-1-sentence ugly, since
it moves the cursor far away if the sentence begins with a comment.
While this is true, *today*, there is no need to undo the last sentence
with the button to edit the text. One can just move the cursor where he
likes and edit. In this case the sentence is backtracked automatically
and the cursor is left where it is.
Hence considering initial comments as part of the following sentence
should not be an usability issue anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- the zone to be edited is now between the marks
start_of_input and stop_of_input
- when -debug is given, the edit zone is underlined
- the cmd_stack is focused/unfocused according to the new protocol
- read only tag resurrected and used to block the "Qed" ending
a focused zone
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
That is pretty tricky, and is not as nice I would like
for to_process text (that is still considered as locked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16453 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16321 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
The handler for apply_tag removed in commit 16044 was probaly meant
for that. We now proceed in a more simple way, in Sentence.split_slice_lax,
instead of doing a remove_tag in a apply_tag handler (!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
It seemed to intrusive to have it display the text underlined and red.
The goal of this tag is to notify the user when Coq doesn't guarantee
correctness, not to make the command look like an error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15759 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
And that's all !
It erase the possibility of code folding...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
code that used to serve as such a long time ago.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15234 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15101 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Lexing send back an offset couple delimiting beginning and
ending of sentences. This couple is used to apply a tag on the whole
sentence.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12808 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Sentences are locked up to the period, and it's now possible to eval
when there is no final whitespace. CoqIde will refuse to evaluate
further if there is no whitespace, though.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12539 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sentence extraction and proof folding is now done with tags. The lexer
has been modified to use a callback to "stamp" the lexical constructs
that must be distinguished.
new funcs in ide/coqide.ml :
apply_tag : GText.buffer -> GText.iter -> (int -> int) ->
int -> int -> CoqLex.token -> unit
remove_tags : GText.buffer -> GText.iter -> GText.iter -> unit
tag_slice : GText.buffer -> GText.iter -> GText.iter ->
(GText.buffer -> GText.iter -> GText.iter) -> unit
get_sentence_bounds : GText.iter -> GText.iter * GText.iter
end_tag_present : GText.iter -> bool
tag_on_insert : GText.buffer -> unit
force_retag : GText.buffer -> unit
toggle_proof_visibility : GText.buffer -> GText.iter -> unit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12517 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
tags with the same name. This fixes file opening.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12396 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
all tags are isolated in tags.ml, and all tags are accessed directly,
not through their names.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12327 85f007b7-540e-0410-9357-904b9bb8a0f7
|