--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat Mar 28 15:40:47 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Apr 06 19:04:38 2009 +0200
@@ -38,23 +38,27 @@
"`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
"[()\\[\\]{}:;]", Pattern.MULTILINE)
- val empty = new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false)
+ val empty =
+ new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet.empty, LinearSet.empty, false, _ => false)
}
-class ProofDocument(val tokens: LinearSet[Token],
+class ProofDocument(val id: String,
+ val tokens: LinearSet[Token],
val commands: LinearSet[Command],
val active: Boolean,
is_command_keyword: String => Boolean)
{
- def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
+ def mark_active: ProofDocument =
+ new ProofDocument(id, tokens, commands, true, is_command_keyword)
def activate: (ProofDocument, StructureChange) = {
- val (doc, change) = text_changed(new Text.Change(0, 0, content, content.length))
+ 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(tokens, commands, active, f)
+ new ProofDocument(id, tokens, commands, active, f)
def content = Token.string_from_tokens(List() ++ tokens)
/** token view **/
@@ -105,13 +109,11 @@
}
}
val insert = new_tokens.reverse
- val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
-
- token_changed(begin.lastOption,
+ val new_token_list = begin ::: insert ::: old_suffix
+ token_changed(change.id,
insert,
removed,
- new_tokenset,
- old_suffix.firstOption)
+ new_token_list)
}
/** command view **/
@@ -121,40 +123,32 @@
return null
}
- private def token_changed(before_change: Option[Token],
+ private def token_changed(new_id: String,
inserted_tokens: List[Token],
removed_tokens: List[Token],
- new_tokenset: LinearSet[Token],
- after_change: Option[Token]): (ProofDocument, StructureChange) =
+ new_token_list: List[Token]): (ProofDocument, StructureChange) =
{
- val commands = List() ++ this.commands
+ val commands = List[Command]() ++ this.commands
+
+ // calculate removed commands
+ val first_removed = removed_tokens.firstOption
+ val last_removed = removed_tokens.lastOption
+
val (begin, remaining) =
- before_change match {
- case None => (Nil, commands)
- case Some(bc) => commands.break(_.tokens.contains(bc))
- }
- val (_removed, _end) =
- after_change match {
- case None => (remaining, Nil)
- case Some(ac) => remaining.break(_.tokens.contains(ac))
+ first_removed match {
+ case None => (Nil: List[Command], commands)
+ case Some(fr) => commands.break(_.tokens.contains(fr))
}
- val (removed, end) = _end match {
- case Nil => (_removed, Nil)
- case acc::end => if (after_change.isDefined && after_change.get.kind == Token.Kind.COMMAND_START)
- (_removed, _end)
- else (_removed ::: List(acc), end)
- }
- val all_removed_tokens = for(c <- removed; t <- c.tokens) yield t
- val (pseudo_new_pre, rest) =
- if (! before_change.isDefined) (Nil, all_removed_tokens)
- else {
- val (a, b) = all_removed_tokens.span (_ != before_change.get)
- b match {
- case Nil => (a, Nil)
- case bc::rest => (a ::: List(bc), b)
- }
+ val removed: 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 pseudo_new_post = rest.dropWhile(Some(_) != after_change)
def tokens_to_commands(tokens: List[Token]): List[Command]= {
tokens match {
@@ -165,13 +159,24 @@
}
}
- val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
+ // calculate inserted commands
+ val first_inserted = inserted_tokens.firstOption
+ val last_inserted = inserted_tokens.lastOption
+
+ val new_commands = tokens_to_commands(new_token_list)
- val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
+ // drop known commands from the beginning
+ val after_change = new_commands
+ val inserted_commands = new_commands.dropWhile(_.tokens.contains(first_inserted))
+
+ val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
+ val new_commandset = (LinearSet() ++ (new_commands)).asInstanceOf[LinearSet[Command]]
+
val before = begin match {case Nil => None case _ => Some (begin.last)}
+ val change = new StructureChange(None,List() ++ new_commandset, removed)
- val change = new StructureChange(before, new_commands, removed)
- val doc = new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword)
+ val doc =
+ new ProofDocument(new_id, new_tokenset, new_commandset, active, is_command_keyword)
return (doc, change)
}
}