--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Feb 19 20:44:28 2009 +0100
@@ -32,10 +32,9 @@
val prover_setup = Isabelle.plugin.prover_setup(buffer)
if (prover_setup.isDefined) {
val document = prover_setup.get.prover.document
- val commands = document.commands
- while (!stopped && commands.hasNext) {
- data.root.add(commands.next.root_node.swing_node)
- }
+ for (command <- document.commands)
+ data.root.add(command.root_node.swing_node)
+
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
} else {
data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
@@ -51,7 +50,7 @@
override def canCompleteAnywhere = true
override def getInstantCompletionTriggers = "\\"
- override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
+ override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{
val buffer = pane.getBuffer
val ps = Isabelle.prover_setup(buffer)
if (ps.isDefined) {
@@ -83,7 +82,7 @@
}
return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
} else return null
- }
+ }*/
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Feb 19 20:44:28 2009 +0100
@@ -46,7 +46,7 @@
buffer.addBufferListener(this)
- private var col: Text.Changed = null
+ private var col: Text.Change = null
private val col_timer = new Timer(300, new ActionListener() {
override def actionPerformed(e: ActionEvent) = commit
@@ -88,6 +88,7 @@
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
update_styles
+ changes.event(new Text.Change(0,buffer.getText(0, buffer.getLength),0))
}
def deactivate() = {
@@ -104,14 +105,14 @@
def from_current (pos: Int) =
if (col != null && col.start <= pos)
- if (pos < col.start + col.added) col.start
- else pos - col.added + col.removed
+ if (pos < col.start + col.added.length) col.start
+ else pos - col.added.length + col.removed
else pos
def to_current (pos : Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.removed) col.start
- else pos + col.added - col.removed
+ else pos + col.added.length - col.removed
else pos
def repaint(cmd: Command) =
@@ -162,9 +163,10 @@
val metrics = text_area.getPainter.getFontMetrics
var e = prover.document.find_command_at(from_current(start))
-
+ val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)).
+ takeWhile(c => to_current(c.start) < end)
// encolor phase
- while (e != null && to_current(e.start) < end) {
+ for (e <- commands) {
val begin = start max to_current(e.start)
val finish = end - 1 min to_current(e.stop)
encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
@@ -178,7 +180,6 @@
DynamicTokenMarker.choose_color(node.kind), true)
}
}
- e = e.next
}
gfx.setColor(saved_color)
@@ -189,7 +190,7 @@
def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
def length = buffer.getLength
- val changes = new EventBus[Text.Changed]
+ val changes = new EventBus[Text.Change]
/* BufferListener methods */
@@ -219,13 +220,14 @@
override def preContentInserted(buffer: JEditBuffer,
start_line: Int, offset: Int, num_lines: Int, length: Int) =
{
+ val text = buffer.getText(offset, length)
if (col == null)
- col = new Text.Changed(offset, length, 0)
- else if (col.start <= offset && offset <= col.start + col.added)
- col = new Text.Changed(col.start, col.added + length, col.removed)
+ col = new Text.Change(offset, text, 0)
+ else if (col.start <= offset && offset <= col.start + col.added.length)
+ col = new Text.Change(col.start, col.added + text, col.removed)
else {
commit
- col = new Text.Changed(offset, length, 0)
+ col = new Text.Change(offset, text, 0)
}
delay_commit
}
@@ -234,20 +236,22 @@
start_line: Int, start: Int, num_lines: Int, removed: Int) =
{
if (col == null)
- col = new Text.Changed(start, 0, removed)
- else if (col.start > start + removed || start > col.start + col.added) {
+ col = new Text.Change(start, "", removed)
+ else if (col.start > start + removed || start > col.start + col.added.length) {
commit
- col = new Text.Changed(start, 0, removed)
+ col = new Text.Change(start, "", removed)
}
else {
- val offset = start - col.start
- val diff = col.added - removed
+/* val offset = start - col.start
+ val diff = col.added.length - removed
val (added, add_removed) =
if (diff < offset)
(offset max 0, diff - (offset max 0))
else
(diff - (offset min 0), offset min 0)
- col = new Text.Changed(start min col.start, added, col.removed - add_removed)
+ col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
+ commit
+ col = new Text.Change(start, "", removed)
}
delay_commit
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Feb 19 20:44:28 2009 +0100
@@ -7,13 +7,13 @@
package isabelle.proofdocument
-
+import scala.collection.mutable.ListBuffer
import java.util.regex.Pattern
import isabelle.prover.{Prover, Command}
case class StructureChange(
- val before_change: Command,
+ val before_change: Option[Command],
val added_commands: List[Command],
val removed_commands: List[Command])
@@ -39,69 +39,45 @@
class ProofDocument(text: Text, is_command_keyword: String => Boolean)
{
- private var active = false
+ private var active = false
def activate() {
if (!active) {
active = true
- text_changed(0, text.length, 0)
+ text_changed(new Text.Change(0, content, content.length))
}
}
- text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
+ text.changes += (change => text_changed(change))
-
-
+ var tokens = Nil : List[Token]
+ var commands = Nil : List[Command]
+ def content = Token.string_from_tokens(tokens)
/** token view **/
- private var first_token: Token = null
- private var last_token: Token = null
-
- private def tokens(start: Token, stop: Token) = new Iterator[Token] {
- var current = start
- def hasNext = current != stop && current != null
- def next() = { val save = current; current = current.next; save }
- }
- private def tokens(start: Token): Iterator[Token] = tokens(start, null)
- private def tokens(): Iterator[Token] = tokens(first_token, null)
-
-
- private def text_changed(start: Int, added_len: Int, removed_len: Int)
+ private def text_changed(change: Text.Change)
{
- if (!active)
- return
+ val (begin, remaining) = tokens.span(_.stop < change.start)
+ val (removed, end) = remaining.span(_.start <= change.start + change.removed)
+ for (t <- end) t.start += (change.added.length - change.removed)
- var before_change =
- if (Token.check_stop(first_token, _ < start)) Token.scan(first_token, _.stop >= start)
- else null
-
- var first_removed =
- if (before_change != null) before_change.next
- else if (Token.check_start(first_token, _ <= start + removed_len)) first_token
- else null
-
- var last_removed = Token.scan(first_removed, _.start > start + removed_len)
+ val split_begin = removed.takeWhile(_.start < change.start).
+ map (t => new Token(t.start,
+ t.content.substring(0, change.start - t.start),
+ 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))
- var shift_token =
- if (last_removed != null) last_removed
- else if (Token.check_start(first_token, _ > start)) first_token
- else null
-
- while (shift_token != null) {
- shift_token.shift(added_len - removed_len, start)
- shift_token = shift_token.next
- }
-
- // scan changed tokens until the end of the text or a matching token is
- // found which is beyond the changed area
- val match_start = if (before_change == null) 0 else before_change.stop
- var first_added: Token = null
- var last_added: Token = null
+ var invalid_tokens = split_begin :::
+ new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
+ var new_tokens = Nil: List[Token]
+ var old_suffix = Nil: List[Token]
- val matcher = ProofDocument.token_pattern.matcher(text.content(match_start, text.length))
- var finished = false
- var position = 0
- while (matcher.find(position) && !finished) {
- position = matcher.end
+ val match_start = invalid_tokens.first.start
+ val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
+
+ while (matcher.find() && invalid_tokens != Nil) {
val kind =
if (is_command_keyword(matcher.group))
Token.Kind.COMMAND_START
@@ -109,251 +85,89 @@
Token.Kind.COMMENT
else
Token.Kind.OTHER
- val new_token = new Token(matcher.start + match_start, matcher.end + match_start, kind)
-
- if (first_added == null)
- first_added = new_token
- else {
- new_token.prev = last_added
- last_added.next = new_token
- }
- last_added = new_token
-
- while (Token.check_stop(last_removed, _ < new_token.stop) &&
- last_removed.next != null)
- last_removed = last_removed.next
-
- if (new_token.stop >= start + added_len &&
- Token.check_stop(last_removed, _ == new_token.stop))
- finished = true
- }
+ val new_token = new Token(match_start + matcher.start, matcher.group, kind)
+ new_tokens ::= new_token
- var after_change = if (last_removed != null) last_removed.next else null
-
- // remove superflous first token-change
- if (first_added != null && first_added == first_removed &&
- first_added.stop < start) {
- before_change = first_removed
- if (last_removed == first_removed) {
- last_removed = null
- first_removed = null
- }
- else {
- first_removed = first_removed.next
- assert(first_removed != null)
- }
-
- if (last_added == first_added) {
- last_added = null
- first_added = null
- }
- if (first_added != null)
- first_added = first_added.next
- }
-
- // remove superflous last token-change
- if (last_added != null && last_added == last_removed &&
- last_added.start > start + added_len) {
- after_change = last_removed
- if (first_removed == last_removed) {
- first_removed = null
- last_removed = null
- }
- else {
- last_removed = last_removed.prev
- assert(last_removed != null)
+ invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
+ invalid_tokens match {
+ case t::ts => if(t.start == new_token.start &&
+ t.start > change.start + change.added.length) {
+ old_suffix = ts
+ invalid_tokens = Nil
+ }
+ case _ =>
}
-
- if (last_added == first_added) {
- last_added = null
- first_added = null
- }
- else
- last_added = last_added.prev
}
-
- if (first_removed == null && first_added == null)
- return
-
- if (first_token == null) {
- first_token = first_added
- last_token = last_added
- }
- else {
- // cut removed tokens out of list
- if (first_removed != null)
- first_removed.prev = null
- if (last_removed != null)
- last_removed.next = null
-
- if (first_token == first_removed)
- if (first_added != null)
- first_token = first_added
- else
- first_token = after_change
-
- if (last_token == last_removed)
- if (last_added != null)
- last_token = last_added
- else
- last_token = before_change
-
- // insert new tokens into list
- if (first_added != null) {
- first_added.prev = before_change
- if (before_change != null)
- before_change.next = first_added
- else
- first_token = first_added
- }
- else if (before_change != null)
- before_change.next = after_change
-
- if (last_added != null) {
- last_added.next = after_change
- if (after_change != null)
- after_change.prev = last_added
- else
- last_token = last_added
- }
- else if (after_change != null)
- after_change.prev = before_change
- }
-
- token_changed(before_change, after_change, first_removed)
+ val insert = new_tokens.reverse
+ tokens = begin ::: insert ::: old_suffix
+
+ token_changed(begin.lastOption,
+ insert,
+ removed,
+ old_suffix.firstOption)
}
-
-
/** command view **/
val structural_changes = new EventBus[StructureChange]
- def commands_from(start: Token) = new Iterator[Command] {
- var current = start
- def hasNext = current != null
- def next = { val s = current.command ; current = s.last.next ; s }
- }
- def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
- def commands = commands_from(first_token)
-
def find_command_at(pos: Int): Command = {
for (cmd <- commands) { if (pos < cmd.stop) return cmd }
return null
}
- private def token_changed(start: Token, stop: Token, removed: Token)
+ private def token_changed(before_change: Option[Token],
+ inserted_tokens: List[Token],
+ removed_tokens: List[Token],
+ after_change: Option[Token])
{
- var removed_commands: List[Command] = Nil
- var first: Command = null
- var last: Command = null
-
- for (t <- tokens(removed)) {
- if (first == null)
- first = t.command
- if (t.command != last)
- removed_commands = t.command :: removed_commands
- last = t.command
+ 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))
+ }
+ 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)
}
-
- var before: Command = null
- if (!removed_commands.isEmpty) {
- if (first.first == removed) {
- if (start == null)
- before = null
- else
- before = start.command
+ 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)
+ }
}
- else
- before = first.prev
- }
+ val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
- var added_commands: List[Command] = Nil
- var scan: Token = null
- if (start != null) {
- val next = start.next
- if (first != null && first.first != removed) {
- scan = first.first
- if (before == null)
- before = first.prev
- }
- else if (next != null && next != stop) {
- if (next.kind == Token.Kind.COMMAND_START) {
- before = start.command
- scan = next
- }
- else if (first == null || first.first == removed) {
- first = start.command
- removed_commands = first :: removed_commands
- scan = first.first
- if (before == null)
- before = first.prev
- }
- else {
- scan = first.first
- if (before == null)
- before = first.prev
- }
+ def tokens_to_commands(tokens: List[Token]): List[Command]= {
+ tokens match {
+ case Nil => Nil
+ case t::ts =>
+ val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
+ new Command(t::cmd) :: tokens_to_commands (rest)
}
}
- else
- scan = first_token
- var stop_scan: Token = null
- if (stop != null) {
- if (stop == stop.command.first)
- stop_scan = stop
- else
- stop_scan = stop.command.last.next
- }
- else if (last != null)
- stop_scan = last.last.next
- else
- stop_scan = null
-
- var cmd_start: Token = null
- var cmd_stop: Token = null
- var overrun = false
- var finished = false
- while (scan != null && !finished) {
- if (scan == stop_scan) {
- if (scan.kind == Token.Kind.COMMAND_START)
- finished = true
- else
- overrun = true
- }
+ System.err.println("ins_tokens: " + inserted_tokens)
+ val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
+ System.err.println("new_commands: " + new_commands)
- if (scan.kind == Token.Kind.COMMAND_START && cmd_start != null && !finished) {
- if (!overrun) {
- added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
- cmd_start = scan
- cmd_stop = scan
- }
- else
- finished = true
- }
- else if (!finished) {
- if (cmd_start == null)
- cmd_start = scan
- cmd_stop = scan
- }
- if (overrun && !finished) {
- if (scan.command != last)
- removed_commands = scan.command :: removed_commands
- last = scan.command
- }
-
- if (!finished)
- scan = scan.next
- }
-
- if (cmd_start != null)
- added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
-
- // relink commands
- added_commands = added_commands.reverse
- removed_commands = removed_commands.reverse
-
- structural_changes.event(new StructureChange(before, added_commands, removed_commands))
+ commands = begin ::: new_commands ::: end
+ val before = begin match {case Nil => None case _ => Some (begin.last)}
+ structural_changes.event(new StructureChange(before, new_commands, removed))
+/*
+ val old = commands
+ commands = tokens_to_commands(tokens)
+ structural_changes.event(new StructureChange(None, commands, old)) */
}
}
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Thu Feb 19 20:44:28 2009 +0100
@@ -8,11 +8,11 @@
object Text {
- case class Changed(val start: Int, val added: Int, val removed: Int)
+ case class Change(start: Int, val added: String, val removed: Int) {
+ override def toString = "start: " + start + " added: " + added + " removed: " + removed
+ }
}
trait Text {
- def content(start: Int, stop: Int): String
- def length: Int
- def changes: EventBus[Text.Changed]
+ def changes: EventBus[Text.Change]
}
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Thu Feb 19 20:44:28 2009 +0100
@@ -18,43 +18,28 @@
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) }
+ 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)
- def scan(s: Token, f: Token => Boolean): Token =
- {
- var current = s
- while (current != null) {
- val next = current.next
- if (next == null || f(next)) return current
- current = next
+ 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 = {
+ 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))
+ )._1
}
- return null
}
+
}
-class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value)
-{
- var next: Token = null
- var prev: Token = null
- var command: Command = null
-
- def length = stop - start
-
- def shift(offset: Int, bottom_clamp: Int) {
- start = bottom_clamp max (start + offset)
- stop = bottom_clamp max (stop + offset)
- }
-
- override def hashCode: Int = (31 + start) * 31 + stop
-
- override def equals(obj: Any): Boolean =
- {
- if (super.equals(obj)) return true
- if (null == obj) return false
- obj match {
- case other: Token => (start == other.start) && (stop == other.stop)
- case other: Any => false
- }
- }
+class Token(var start: Int, val content: String, val kind: Token.Kind.Value) {
+ val length = content.length
+ def stop = start + length
+ override def toString = content + "(" + kind + ")"
}
--- a/src/Tools/jEdit/src/prover/Command.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Thu Feb 19 20:44:28 2009 +0100
@@ -29,40 +29,19 @@
}
-class Command(text: Text, val first: Token, val last: Token)
+class Command(val tokens: List[Token])
{
val id = Isabelle.plugin.id()
-
/* content */
- {
- var t = first
- while (t != null) {
- t.command = this
- t = if (t == last) null else t.next
- }
- }
-
override def toString = name
- val name = text.content(first.start, first.stop)
- val content = text.content(proper_start, proper_stop)
-
- def next = if (last.next != null) last.next.command else null
- def prev = if (first.prev != null) first.prev.command else null
-
- def start = first.start
- def stop = last.stop
+ val name = tokens.head.content
+ val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
- def proper_start = start
- def proper_stop = {
- var i = last
- while (i != first && i.kind == Token.Kind.COMMENT)
- i = i.prev
- i.stop
- }
-
+ def start = tokens.first.start
+ def stop = tokens.last.stop
/* command status */
--- a/src/Tools/jEdit/src/prover/Prover.scala Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Feb 19 20:44:28 2009 +0100
@@ -195,23 +195,19 @@
this.document = new ProofDocument(text, command_decls.contains(_))
process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
- document.structural_changes += (changes => {
+ document.structural_changes += (changes => if(initialized){
for (cmd <- changes.removed_commands) remove(cmd)
- for (cmd <- changes.added_commands) send(cmd)
+ changes.added_commands.foldLeft (changes.before_change) ((p, c) => {send(p, c); Some(c)})
})
- if (initialized) {
- document.activate()
- activated.event(())
- }
}
- private def send(cmd: Command) {
+ private def send(prev: Option[Command], cmd: Command) {
cmd.status = Command.Status.UNPROCESSED
commands.put(cmd.id, cmd)
val content = isabelle_system.symbols.encode(cmd.content)
process.create_command(cmd.id, content)
- process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
+ process.insert_command(prev match {case Some(c) => c.id case None => ""}, cmd.id)
}
def remove(cmd: Command) {