| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12794 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This reverts commit 8162ee31152eb2f99af724e88a7e15a899c17811.
Not the smartest thing to do on the verge of tagging.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12649 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The formatting logic is now isolated in ide/proofBrowser.ml, and the
goal printing logic is deported inside ide/coq.ml. Also, the proof mode
special printing has been cut out. Finally, turn every call to
show_goals_full into show_goals, and use show_goals_full as the body of
show_goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12648 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
|
|
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
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
