src/Tools/jEdit/src/proofdocument/ProofDocument.scala
changeset 34655 77722b866fb4
parent 34653 2e033aaf128e
child 34657 410094a3419b
equal deleted inserted replaced
34654:30f588245884 34655:77722b866fb4
   113           Token.Kind.OTHER
   113           Token.Kind.OTHER
   114       val new_token = new Token(matcher.group, kind)
   114       val new_token = new Token(matcher.group, kind)
   115       start += (new_token -> (match_start + matcher.start))
   115       start += (new_token -> (match_start + matcher.start))
   116       new_tokens ::= new_token
   116       new_tokens ::= new_token
   117 
   117 
   118       invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
   118       invalid_tokens = invalid_tokens dropWhile (stop(_) <= stop(new_token))
   119       invalid_tokens match {
   119       invalid_tokens match {
   120         case t :: ts =>
   120         case t :: ts =>
   121           if (start(t) == start(new_token) &&
   121           if (start(t) == start(new_token) &&
   122               start(t) > change.start + change.added.length) {
   122               start(t) > change.start + change.added.length) {
   123           old_suffix = t :: ts
   123           old_suffix = t :: ts