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

0 files changed, 0 insertions, 0 deletions