new handling for lexical structures.

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

1 files changed, 1 insertions, 1 deletions

diff --git a/ide/ide.mllib b/ide/ide.mllib
index 73c1d0735..a235039b9 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -13,9 +13,9 @@ Config_lexer
 Utf8_convert
 Preferences
 Ideutils
+CoqLex
 Gtk_parsing
 Undo
-Highlight
 Coq
 Coq_commands
 Coq_tactics