# HG changeset patch # User immler@in.tum.de # Date 1240222635 -7200 # Node ID bd2b8fde9e25ef18b94f32d954e02fb09551292f # Parent 171c8c6e5707387ba7b6e323733a564b93ddf208 incomplete changes of immutable tokens and commands diff -r 171c8c6e5707 -r bd2b8fde9e25 src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Apr 16 13:38:03 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Apr 20 12:17:15 2009 +0200 @@ -39,53 +39,63 @@ "[()\\[\\]{}:;]", Pattern.MULTILINE) val empty = - new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet.empty, LinearSet.empty, false, _ => false) + new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet(), Map(), LinearSet(), false, _ => false) } class ProofDocument(val id: String, val tokens: LinearSet[Token], + val token_start: Map[Token, Int], val commands: LinearSet[Command], val active: Boolean, is_command_keyword: String => Boolean) { def mark_active: ProofDocument = - new ProofDocument(id, tokens, commands, true, is_command_keyword) + new ProofDocument(id, tokens, token_start, commands, true, is_command_keyword) def activate: (ProofDocument, StructureChange) = { val (doc, change) = text_changed(new Text.Change(isabelle.jedit.Isabelle.plugin.id(), 0, content, content.length)) return (doc.mark_active, change) } def set_command_keyword(f: String => Boolean): ProofDocument = - new ProofDocument(id, tokens, commands, active, f) + new ProofDocument(id, tokens, token_start, commands, active, f) - def content = Token.string_from_tokens(List() ++ tokens) + def content = Token.string_from_tokens(List() ++ tokens, token_start) /** token view **/ def text_changed(change: Text.Change): (ProofDocument, StructureChange) = { + //indices of tokens + var start: Map[Token, Int] = token_start + def stop(t: Token) = start(t) + t.length + // split old token lists val tokens = List() ++ this.tokens - val (begin, remaining) = tokens.span(_.stop < change.start) - val (removed, end_unshifted) = remaining.span(_.start <= change.start + change.removed) - val end = for (t <- end_unshifted) yield t.shift(change.added.length - change.removed) + val (begin, remaining) = tokens.span(stop(_) < change.start) + val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed) + // update indices + start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed))) + start = removed.foldLeft (start) ((s, t) => s - t) - val split_begin = removed.takeWhile(_.start < change.start). - map (t => new Token(t.start, - t.content.substring(0, change.start - t.start), + val split_begin = removed.takeWhile(start(_) < change.start). + map (t => new Token(t.content.substring(0, change.start - start(t)), + t.kind)) + val split_end = removed.dropWhile(stop(_) < change.start + change.removed). + map (t => new Token(t.content.substring(change.start + change.removed - start(t)), t.kind)) - val split_end = removed.dropWhile(_.stop < change.start + change.removed). - map (t => new Token(change.start + change.added.length, - t.content.substring(change.start + change.removed - t.start), - t.kind)) + // update indices + start = split_end.foldLeft (start) ((s, t) => s + (t -> (change.start + change.added.length))) + val ins = new Token(change.added, Token.Kind.OTHER) + start += (ins -> change.start) + var invalid_tokens = split_begin ::: - new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end + ins :: split_end ::: end var new_tokens = Nil: List[Token] var old_suffix = Nil: List[Token] - val match_start = invalid_tokens.first.start - val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens)) + val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0) + val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) while (matcher.find() && invalid_tokens != Nil) { val kind = @@ -95,13 +105,14 @@ Token.Kind.COMMENT else Token.Kind.OTHER - val new_token = new Token(match_start + matcher.start, matcher.group, kind) + val new_token = new Token(matcher.group, kind) + start += (new_token -> (match_start + matcher.start)) new_tokens ::= new_token - invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop) + invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token)) invalid_tokens match { - case t::ts => if(t.start == new_token.start && - t.start > change.start + change.added.length) { + case t::ts => if(start(t) == start(new_token) && + start(t) > change.start + change.added.length) { old_suffix = ts invalid_tokens = Nil } @@ -115,7 +126,8 @@ insert, removed, old_suffix.firstOption, - new_token_list) + new_token_list, + start) } /** command view **/ @@ -130,28 +142,23 @@ inserted_tokens: List[Token], removed_tokens: List[Token], after_change: Option[Token], - new_token_list: List[Token]): (ProofDocument, StructureChange) = + new_token_list: List[Token], + new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) = { - val commands = List[Command]() ++ this.commands + val commands_list = List[Command]() ++ commands // calculate removed commands val first_removed = removed_tokens.firstOption - val last_removed = removed_tokens.lastOption val (begin, remaining) = first_removed match { - case None => (Nil: List[Command], commands) - case Some(fr) => commands.break(_.tokens.contains(fr)) + case None => (Nil, commands_list) + case Some(fr) => commands_list.break(_.tokens.contains(fr)) } - val removed_commands: List[Command]= - last_removed match { - case None => Nil - case Some(lr) => - remaining.takeWhile(!_.tokens.contains(lr)) ++ - (remaining.find(_.tokens.contains(lr)) match { - case None => Nil - case Some(x) => List(x) - }) + val (removed_commands, end) = + after_change match { + case None => (remaining, Nil) + case Some(ac) => remaining.break(_.tokens.contains(ac)) } def tokens_to_commands(tokens: List[Token]): List[Command]= { @@ -180,13 +187,13 @@ case None => changed_commands case Some(ac) => changed_commands.takeWhile(!_.tokens.contains(ac)) } - //val change = new StructureChange(new_commands.find(_.tokens.contains(before_change)), - // inserted_commands, removed_commands) - // TODO: revert to upper change, when commands and tokens are ok - val change = new StructureChange(None, List() ++ new_commandset, commands) + val change = new StructureChange(new_commands.find(_.tokens.contains(before_change)), + inserted_commands, removed_commands) // build new document + var new_commands = commands + while(new_commands.next()) val doc = - new ProofDocument(new_id, new_tokenset, new_commandset, active, is_command_keyword) + new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword) return (doc, change) } } diff -r 171c8c6e5707 -r bd2b8fde9e25 src/Tools/jEdit/src/proofdocument/Token.scala --- a/src/Tools/jEdit/src/proofdocument/Token.scala Thu Apr 16 13:38:03 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Mon Apr 20 12:17:15 2009 +0200 @@ -18,30 +18,25 @@ val OTHER = Value("OTHER") } - def check_start(t: Token, P: Int => Boolean) = t != null && P(t.start) - def check_stop(t: Token, P: Int => Boolean) = t != null && P(t.stop) - private def fill(n: Int) = { val blanks = new Array[Char](n) for(i <- 0 to n - 1) blanks(i) = ' ' new String(blanks) } - def string_from_tokens (tokens: List[Token]): String = { + def string_from_tokens (tokens: List[Token], starts: Map[Token, Int]): String = { + def stop(t: Token) = starts(t) + t.length tokens match { case Nil => "" - case t::tokens => (tokens.foldLeft - (t.content, t.stop) - ((a, token) => (a._1 + fill(token.start - a._2) + token.content, token.stop)) + case t::tokens => ( tokens.foldLeft + (t.content, stop(t)) + ((a, token) => (a._1 + fill(starts(token) - a._2) + token.content, stop(token))) )._1 } } } -class Token(val start: Int, val content: String, val kind: Token.Kind.Value) { +class Token(val content: String, val kind: Token.Kind.Value) { val length = content.length - val stop = start + length override def toString = content + "(" + kind + ")" - override def hashCode: Int = (31 + start) * 31 + stop - def shift(i: Int) = new Token(start + i, content, kind) }