1.1 --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Feb 05 21:18:30 2009 +0100
1.2 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Feb 19 20:44:28 2009 +0100
1.3 @@ -32,10 +32,9 @@
1.4 val prover_setup = Isabelle.plugin.prover_setup(buffer)
1.5 if (prover_setup.isDefined) {
1.6 val document = prover_setup.get.prover.document
1.7 - val commands = document.commands
1.8 - while (!stopped && commands.hasNext) {
1.9 - data.root.add(commands.next.root_node.swing_node)
1.10 - }
1.11 + for (command <- document.commands)
1.12 + data.root.add(command.root_node.swing_node)
1.13 +
1.14 if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
1.15 } else {
1.16 data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
1.17 @@ -51,7 +50,7 @@
1.18 override def canCompleteAnywhere = true
1.19 override def getInstantCompletionTriggers = "\\"
1.20
1.21 - override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
1.22 + override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{
1.23 val buffer = pane.getBuffer
1.24 val ps = Isabelle.prover_setup(buffer)
1.25 if (ps.isDefined) {
1.26 @@ -83,7 +82,7 @@
1.27 }
1.28 return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
1.29 } else return null
1.30 - }
1.31 + }*/
1.32
1.33 }
1.34
2.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Feb 05 21:18:30 2009 +0100
2.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Feb 19 20:44:28 2009 +0100
2.3 @@ -46,7 +46,7 @@
2.4 buffer.addBufferListener(this)
2.5
2.6
2.7 - private var col: Text.Changed = null
2.8 + private var col: Text.Change = null
2.9
2.10 private val col_timer = new Timer(300, new ActionListener() {
2.11 override def actionPerformed(e: ActionEvent) = commit
2.12 @@ -88,6 +88,7 @@
2.13 text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
2.14 buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
2.15 update_styles
2.16 + changes.event(new Text.Change(0,buffer.getText(0, buffer.getLength),0))
2.17 }
2.18
2.19 def deactivate() = {
2.20 @@ -104,14 +105,14 @@
2.21
2.22 def from_current (pos: Int) =
2.23 if (col != null && col.start <= pos)
2.24 - if (pos < col.start + col.added) col.start
2.25 - else pos - col.added + col.removed
2.26 + if (pos < col.start + col.added.length) col.start
2.27 + else pos - col.added.length + col.removed
2.28 else pos
2.29
2.30 def to_current (pos : Int) =
2.31 if (col != null && col.start <= pos)
2.32 if (pos < col.start + col.removed) col.start
2.33 - else pos + col.added - col.removed
2.34 + else pos + col.added.length - col.removed
2.35 else pos
2.36
2.37 def repaint(cmd: Command) =
2.38 @@ -162,9 +163,10 @@
2.39
2.40 val metrics = text_area.getPainter.getFontMetrics
2.41 var e = prover.document.find_command_at(from_current(start))
2.42 -
2.43 + val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)).
2.44 + takeWhile(c => to_current(c.start) < end)
2.45 // encolor phase
2.46 - while (e != null && to_current(e.start) < end) {
2.47 + for (e <- commands) {
2.48 val begin = start max to_current(e.start)
2.49 val finish = end - 1 min to_current(e.stop)
2.50 encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
2.51 @@ -178,7 +180,6 @@
2.52 DynamicTokenMarker.choose_color(node.kind), true)
2.53 }
2.54 }
2.55 - e = e.next
2.56 }
2.57
2.58 gfx.setColor(saved_color)
2.59 @@ -189,7 +190,7 @@
2.60
2.61 def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
2.62 def length = buffer.getLength
2.63 - val changes = new EventBus[Text.Changed]
2.64 + val changes = new EventBus[Text.Change]
2.65
2.66
2.67 /* BufferListener methods */
2.68 @@ -219,13 +220,14 @@
2.69 override def preContentInserted(buffer: JEditBuffer,
2.70 start_line: Int, offset: Int, num_lines: Int, length: Int) =
2.71 {
2.72 + val text = buffer.getText(offset, length)
2.73 if (col == null)
2.74 - col = new Text.Changed(offset, length, 0)
2.75 - else if (col.start <= offset && offset <= col.start + col.added)
2.76 - col = new Text.Changed(col.start, col.added + length, col.removed)
2.77 + col = new Text.Change(offset, text, 0)
2.78 + else if (col.start <= offset && offset <= col.start + col.added.length)
2.79 + col = new Text.Change(col.start, col.added + text, col.removed)
2.80 else {
2.81 commit
2.82 - col = new Text.Changed(offset, length, 0)
2.83 + col = new Text.Change(offset, text, 0)
2.84 }
2.85 delay_commit
2.86 }
2.87 @@ -234,20 +236,22 @@
2.88 start_line: Int, start: Int, num_lines: Int, removed: Int) =
2.89 {
2.90 if (col == null)
2.91 - col = new Text.Changed(start, 0, removed)
2.92 - else if (col.start > start + removed || start > col.start + col.added) {
2.93 + col = new Text.Change(start, "", removed)
2.94 + else if (col.start > start + removed || start > col.start + col.added.length) {
2.95 commit
2.96 - col = new Text.Changed(start, 0, removed)
2.97 + col = new Text.Change(start, "", removed)
2.98 }
2.99 else {
2.100 - val offset = start - col.start
2.101 - val diff = col.added - removed
2.102 +/* val offset = start - col.start
2.103 + val diff = col.added.length - removed
2.104 val (added, add_removed) =
2.105 if (diff < offset)
2.106 (offset max 0, diff - (offset max 0))
2.107 else
2.108 (diff - (offset min 0), offset min 0)
2.109 - col = new Text.Changed(start min col.start, added, col.removed - add_removed)
2.110 + col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
2.111 + commit
2.112 + col = new Text.Change(start, "", removed)
2.113 }
2.114 delay_commit
2.115 }
3.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Feb 05 21:18:30 2009 +0100
3.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Feb 19 20:44:28 2009 +0100
3.3 @@ -7,13 +7,13 @@
3.4
3.5 package isabelle.proofdocument
3.6
3.7 -
3.8 +import scala.collection.mutable.ListBuffer
3.9 import java.util.regex.Pattern
3.10 import isabelle.prover.{Prover, Command}
3.11
3.12
3.13 case class StructureChange(
3.14 - val before_change: Command,
3.15 + val before_change: Option[Command],
3.16 val added_commands: List[Command],
3.17 val removed_commands: List[Command])
3.18
3.19 @@ -39,69 +39,45 @@
3.20
3.21 class ProofDocument(text: Text, is_command_keyword: String => Boolean)
3.22 {
3.23 - private var active = false
3.24 + private var active = false
3.25 def activate() {
3.26 if (!active) {
3.27 active = true
3.28 - text_changed(0, text.length, 0)
3.29 + text_changed(new Text.Change(0, content, content.length))
3.30 }
3.31 }
3.32
3.33 - text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
3.34 + text.changes += (change => text_changed(change))
3.35
3.36 -
3.37 -
3.38 + var tokens = Nil : List[Token]
3.39 + var commands = Nil : List[Command]
3.40 + def content = Token.string_from_tokens(tokens)
3.41 /** token view **/
3.42
3.43 - private var first_token: Token = null
3.44 - private var last_token: Token = null
3.45 -
3.46 - private def tokens(start: Token, stop: Token) = new Iterator[Token] {
3.47 - var current = start
3.48 - def hasNext = current != stop && current != null
3.49 - def next() = { val save = current; current = current.next; save }
3.50 - }
3.51 - private def tokens(start: Token): Iterator[Token] = tokens(start, null)
3.52 - private def tokens(): Iterator[Token] = tokens(first_token, null)
3.53 + private def text_changed(change: Text.Change)
3.54 + {
3.55 + val (begin, remaining) = tokens.span(_.stop < change.start)
3.56 + val (removed, end) = remaining.span(_.start <= change.start + change.removed)
3.57 + for (t <- end) t.start += (change.added.length - change.removed)
3.58
3.59 + val split_begin = removed.takeWhile(_.start < change.start).
3.60 + map (t => new Token(t.start,
3.61 + t.content.substring(0, change.start - t.start),
3.62 + t.kind))
3.63 + val split_end = removed.dropWhile(_.stop < change.start + change.removed).
3.64 + map (t => new Token(change.start + change.added.length,
3.65 + t.content.substring(change.start + change.removed - t.start),
3.66 + t.kind))
3.67
3.68 - private def text_changed(start: Int, added_len: Int, removed_len: Int)
3.69 - {
3.70 - if (!active)
3.71 - return
3.72 + var invalid_tokens = split_begin :::
3.73 + new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
3.74 + var new_tokens = Nil: List[Token]
3.75 + var old_suffix = Nil: List[Token]
3.76
3.77 - var before_change =
3.78 - if (Token.check_stop(first_token, _ < start)) Token.scan(first_token, _.stop >= start)
3.79 - else null
3.80 -
3.81 - var first_removed =
3.82 - if (before_change != null) before_change.next
3.83 - else if (Token.check_start(first_token, _ <= start + removed_len)) first_token
3.84 - else null
3.85 + val match_start = invalid_tokens.first.start
3.86 + val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
3.87
3.88 - var last_removed = Token.scan(first_removed, _.start > start + removed_len)
3.89 -
3.90 - var shift_token =
3.91 - if (last_removed != null) last_removed
3.92 - else if (Token.check_start(first_token, _ > start)) first_token
3.93 - else null
3.94 -
3.95 - while (shift_token != null) {
3.96 - shift_token.shift(added_len - removed_len, start)
3.97 - shift_token = shift_token.next
3.98 - }
3.99 -
3.100 - // scan changed tokens until the end of the text or a matching token is
3.101 - // found which is beyond the changed area
3.102 - val match_start = if (before_change == null) 0 else before_change.stop
3.103 - var first_added: Token = null
3.104 - var last_added: Token = null
3.105 -
3.106 - val matcher = ProofDocument.token_pattern.matcher(text.content(match_start, text.length))
3.107 - var finished = false
3.108 - var position = 0
3.109 - while (matcher.find(position) && !finished) {
3.110 - position = matcher.end
3.111 + while (matcher.find() && invalid_tokens != Nil) {
3.112 val kind =
3.113 if (is_command_keyword(matcher.group))
3.114 Token.Kind.COMMAND_START
3.115 @@ -109,251 +85,89 @@
3.116 Token.Kind.COMMENT
3.117 else
3.118 Token.Kind.OTHER
3.119 - val new_token = new Token(matcher.start + match_start, matcher.end + match_start, kind)
3.120 + val new_token = new Token(match_start + matcher.start, matcher.group, kind)
3.121 + new_tokens ::= new_token
3.122
3.123 - if (first_added == null)
3.124 - first_added = new_token
3.125 - else {
3.126 - new_token.prev = last_added
3.127 - last_added.next = new_token
3.128 + invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
3.129 + invalid_tokens match {
3.130 + case t::ts => if(t.start == new_token.start &&
3.131 + t.start > change.start + change.added.length) {
3.132 + old_suffix = ts
3.133 + invalid_tokens = Nil
3.134 + }
3.135 + case _ =>
3.136 }
3.137 - last_added = new_token
3.138 -
3.139 - while (Token.check_stop(last_removed, _ < new_token.stop) &&
3.140 - last_removed.next != null)
3.141 - last_removed = last_removed.next
3.142 -
3.143 - if (new_token.stop >= start + added_len &&
3.144 - Token.check_stop(last_removed, _ == new_token.stop))
3.145 - finished = true
3.146 }
3.147 + val insert = new_tokens.reverse
3.148 + tokens = begin ::: insert ::: old_suffix
3.149
3.150 - var after_change = if (last_removed != null) last_removed.next else null
3.151 -
3.152 - // remove superflous first token-change
3.153 - if (first_added != null && first_added == first_removed &&
3.154 - first_added.stop < start) {
3.155 - before_change = first_removed
3.156 - if (last_removed == first_removed) {
3.157 - last_removed = null
3.158 - first_removed = null
3.159 - }
3.160 - else {
3.161 - first_removed = first_removed.next
3.162 - assert(first_removed != null)
3.163 - }
3.164 -
3.165 - if (last_added == first_added) {
3.166 - last_added = null
3.167 - first_added = null
3.168 - }
3.169 - if (first_added != null)
3.170 - first_added = first_added.next
3.171 - }
3.172 -
3.173 - // remove superflous last token-change
3.174 - if (last_added != null && last_added == last_removed &&
3.175 - last_added.start > start + added_len) {
3.176 - after_change = last_removed
3.177 - if (first_removed == last_removed) {
3.178 - first_removed = null
3.179 - last_removed = null
3.180 - }
3.181 - else {
3.182 - last_removed = last_removed.prev
3.183 - assert(last_removed != null)
3.184 - }
3.185 -
3.186 - if (last_added == first_added) {
3.187 - last_added = null
3.188 - first_added = null
3.189 - }
3.190 - else
3.191 - last_added = last_added.prev
3.192 - }
3.193 -
3.194 - if (first_removed == null && first_added == null)
3.195 - return
3.196 -
3.197 - if (first_token == null) {
3.198 - first_token = first_added
3.199 - last_token = last_added
3.200 - }
3.201 - else {
3.202 - // cut removed tokens out of list
3.203 - if (first_removed != null)
3.204 - first_removed.prev = null
3.205 - if (last_removed != null)
3.206 - last_removed.next = null
3.207 -
3.208 - if (first_token == first_removed)
3.209 - if (first_added != null)
3.210 - first_token = first_added
3.211 - else
3.212 - first_token = after_change
3.213 -
3.214 - if (last_token == last_removed)
3.215 - if (last_added != null)
3.216 - last_token = last_added
3.217 - else
3.218 - last_token = before_change
3.219 -
3.220 - // insert new tokens into list
3.221 - if (first_added != null) {
3.222 - first_added.prev = before_change
3.223 - if (before_change != null)
3.224 - before_change.next = first_added
3.225 - else
3.226 - first_token = first_added
3.227 - }
3.228 - else if (before_change != null)
3.229 - before_change.next = after_change
3.230 -
3.231 - if (last_added != null) {
3.232 - last_added.next = after_change
3.233 - if (after_change != null)
3.234 - after_change.prev = last_added
3.235 - else
3.236 - last_token = last_added
3.237 - }
3.238 - else if (after_change != null)
3.239 - after_change.prev = before_change
3.240 - }
3.241 -
3.242 - token_changed(before_change, after_change, first_removed)
3.243 + token_changed(begin.lastOption,
3.244 + insert,
3.245 + removed,
3.246 + old_suffix.firstOption)
3.247 }
3.248
3.249 -
3.250 -
3.251 /** command view **/
3.252
3.253 val structural_changes = new EventBus[StructureChange]
3.254
3.255 - def commands_from(start: Token) = new Iterator[Command] {
3.256 - var current = start
3.257 - def hasNext = current != null
3.258 - def next = { val s = current.command ; current = s.last.next ; s }
3.259 - }
3.260 - def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
3.261 - def commands = commands_from(first_token)
3.262 -
3.263 def find_command_at(pos: Int): Command = {
3.264 for (cmd <- commands) { if (pos < cmd.stop) return cmd }
3.265 return null
3.266 }
3.267
3.268 - private def token_changed(start: Token, stop: Token, removed: Token)
3.269 + private def token_changed(before_change: Option[Token],
3.270 + inserted_tokens: List[Token],
3.271 + removed_tokens: List[Token],
3.272 + after_change: Option[Token])
3.273 {
3.274 - var removed_commands: List[Command] = Nil
3.275 - var first: Command = null
3.276 - var last: Command = null
3.277 + val (begin, remaining) =
3.278 + before_change match {
3.279 + case None => (Nil, commands)
3.280 + case Some(bc) => commands.break(_.tokens.contains(bc))
3.281 + }
3.282 + val (_removed, _end) =
3.283 + after_change match {
3.284 + case None => (remaining, Nil)
3.285 + case Some(ac) => remaining.break(_.tokens.contains(ac))
3.286 + }
3.287 + val (removed, end) = _end match {
3.288 + case Nil => (_removed, Nil)
3.289 + case acc::end => if (after_change.isDefined && after_change.get.kind == Token.Kind.COMMAND_START)
3.290 + (_removed, _end)
3.291 + else (_removed ::: List(acc), end)
3.292 + }
3.293 + val all_removed_tokens = for(c <- removed; t <- c.tokens) yield t
3.294 + val (pseudo_new_pre, rest) =
3.295 + if (! before_change.isDefined) (Nil, all_removed_tokens)
3.296 + else {
3.297 + val (a, b) = all_removed_tokens.span (_ != before_change.get)
3.298 + b match {
3.299 + case Nil => (a, Nil)
3.300 + case bc::rest => (a ::: List(bc), b)
3.301 + }
3.302 + }
3.303 + val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
3.304
3.305 - for (t <- tokens(removed)) {
3.306 - if (first == null)
3.307 - first = t.command
3.308 - if (t.command != last)
3.309 - removed_commands = t.command :: removed_commands
3.310 - last = t.command
3.311 + def tokens_to_commands(tokens: List[Token]): List[Command]= {
3.312 + tokens match {
3.313 + case Nil => Nil
3.314 + case t::ts =>
3.315 + val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
3.316 + new Command(t::cmd) :: tokens_to_commands (rest)
3.317 + }
3.318 }
3.319
3.320 - var before: Command = null
3.321 - if (!removed_commands.isEmpty) {
3.322 - if (first.first == removed) {
3.323 - if (start == null)
3.324 - before = null
3.325 - else
3.326 - before = start.command
3.327 - }
3.328 - else
3.329 - before = first.prev
3.330 - }
3.331 + System.err.println("ins_tokens: " + inserted_tokens)
3.332 + val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
3.333 + System.err.println("new_commands: " + new_commands)
3.334
3.335 - var added_commands: List[Command] = Nil
3.336 - var scan: Token = null
3.337 - if (start != null) {
3.338 - val next = start.next
3.339 - if (first != null && first.first != removed) {
3.340 - scan = first.first
3.341 - if (before == null)
3.342 - before = first.prev
3.343 - }
3.344 - else if (next != null && next != stop) {
3.345 - if (next.kind == Token.Kind.COMMAND_START) {
3.346 - before = start.command
3.347 - scan = next
3.348 - }
3.349 - else if (first == null || first.first == removed) {
3.350 - first = start.command
3.351 - removed_commands = first :: removed_commands
3.352 - scan = first.first
3.353 - if (before == null)
3.354 - before = first.prev
3.355 - }
3.356 - else {
3.357 - scan = first.first
3.358 - if (before == null)
3.359 - before = first.prev
3.360 - }
3.361 - }
3.362 - }
3.363 - else
3.364 - scan = first_token
3.365 -
3.366 - var stop_scan: Token = null
3.367 - if (stop != null) {
3.368 - if (stop == stop.command.first)
3.369 - stop_scan = stop
3.370 - else
3.371 - stop_scan = stop.command.last.next
3.372 - }
3.373 - else if (last != null)
3.374 - stop_scan = last.last.next
3.375 - else
3.376 - stop_scan = null
3.377 -
3.378 - var cmd_start: Token = null
3.379 - var cmd_stop: Token = null
3.380 - var overrun = false
3.381 - var finished = false
3.382 - while (scan != null && !finished) {
3.383 - if (scan == stop_scan) {
3.384 - if (scan.kind == Token.Kind.COMMAND_START)
3.385 - finished = true
3.386 - else
3.387 - overrun = true
3.388 - }
3.389 -
3.390 - if (scan.kind == Token.Kind.COMMAND_START && cmd_start != null && !finished) {
3.391 - if (!overrun) {
3.392 - added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
3.393 - cmd_start = scan
3.394 - cmd_stop = scan
3.395 - }
3.396 - else
3.397 - finished = true
3.398 - }
3.399 - else if (!finished) {
3.400 - if (cmd_start == null)
3.401 - cmd_start = scan
3.402 - cmd_stop = scan
3.403 - }
3.404 - if (overrun && !finished) {
3.405 - if (scan.command != last)
3.406 - removed_commands = scan.command :: removed_commands
3.407 - last = scan.command
3.408 - }
3.409 -
3.410 - if (!finished)
3.411 - scan = scan.next
3.412 - }
3.413 -
3.414 - if (cmd_start != null)
3.415 - added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
3.416 -
3.417 - // relink commands
3.418 - added_commands = added_commands.reverse
3.419 - removed_commands = removed_commands.reverse
3.420 -
3.421 - structural_changes.event(new StructureChange(before, added_commands, removed_commands))
3.422 + commands = begin ::: new_commands ::: end
3.423 + val before = begin match {case Nil => None case _ => Some (begin.last)}
3.424 + structural_changes.event(new StructureChange(before, new_commands, removed))
3.425 +/*
3.426 + val old = commands
3.427 + commands = tokens_to_commands(tokens)
3.428 + structural_changes.event(new StructureChange(None, commands, old)) */
3.429 }
3.430 }
4.1 --- a/src/Tools/jEdit/src/proofdocument/Text.scala Thu Feb 05 21:18:30 2009 +0100
4.2 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala Thu Feb 19 20:44:28 2009 +0100
4.3 @@ -8,11 +8,11 @@
4.4
4.5
4.6 object Text {
4.7 - case class Changed(val start: Int, val added: Int, val removed: Int)
4.8 + case class Change(start: Int, val added: String, val removed: Int) {
4.9 + override def toString = "start: " + start + " added: " + added + " removed: " + removed
4.10 + }
4.11 }
4.12
4.13 trait Text {
4.14 - def content(start: Int, stop: Int): String
4.15 - def length: Int
4.16 - def changes: EventBus[Text.Changed]
4.17 + def changes: EventBus[Text.Change]
4.18 }
5.1 --- a/src/Tools/jEdit/src/proofdocument/Token.scala Thu Feb 05 21:18:30 2009 +0100
5.2 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Thu Feb 19 20:44:28 2009 +0100
5.3 @@ -18,43 +18,28 @@
5.4 val OTHER = Value("OTHER")
5.5 }
5.6
5.7 - def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) }
5.8 - def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) }
5.9 + def check_start(t: Token, P: Int => Boolean) = t != null && P(t.start)
5.10 + def check_stop(t: Token, P: Int => Boolean) = t != null && P(t.stop)
5.11
5.12 - def scan(s: Token, f: Token => Boolean): Token =
5.13 - {
5.14 - var current = s
5.15 - while (current != null) {
5.16 - val next = current.next
5.17 - if (next == null || f(next)) return current
5.18 - current = next
5.19 + private def fill(n: Int) = {
5.20 + val blanks = new Array[Char](n)
5.21 + for(i <- 0 to n - 1) blanks(i) = ' '
5.22 + new String(blanks)
5.23 + }
5.24 + def string_from_tokens (tokens: List[Token]): String = {
5.25 + tokens match {
5.26 + case Nil => ""
5.27 + case t::tokens => (tokens.foldLeft
5.28 + (t.content, t.stop)
5.29 + ((a, token) => (a._1 + fill(token.start - a._2) + token.content, token.stop))
5.30 + )._1
5.31 }
5.32 - return null
5.33 }
5.34 +
5.35 }
5.36
5.37 -class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value)
5.38 -{
5.39 - var next: Token = null
5.40 - var prev: Token = null
5.41 - var command: Command = null
5.42 -
5.43 - def length = stop - start
5.44 -
5.45 - def shift(offset: Int, bottom_clamp: Int) {
5.46 - start = bottom_clamp max (start + offset)
5.47 - stop = bottom_clamp max (stop + offset)
5.48 - }
5.49 -
5.50 - override def hashCode: Int = (31 + start) * 31 + stop
5.51 -
5.52 - override def equals(obj: Any): Boolean =
5.53 - {
5.54 - if (super.equals(obj)) return true
5.55 - if (null == obj) return false
5.56 - obj match {
5.57 - case other: Token => (start == other.start) && (stop == other.stop)
5.58 - case other: Any => false
5.59 - }
5.60 - }
5.61 +class Token(var start: Int, val content: String, val kind: Token.Kind.Value) {
5.62 + val length = content.length
5.63 + def stop = start + length
5.64 + override def toString = content + "(" + kind + ")"
5.65 }
6.1 --- a/src/Tools/jEdit/src/prover/Command.scala Thu Feb 05 21:18:30 2009 +0100
6.2 +++ b/src/Tools/jEdit/src/prover/Command.scala Thu Feb 19 20:44:28 2009 +0100
6.3 @@ -29,40 +29,19 @@
6.4 }
6.5
6.6
6.7 -class Command(text: Text, val first: Token, val last: Token)
6.8 +class Command(val tokens: List[Token])
6.9 {
6.10 val id = Isabelle.plugin.id()
6.11
6.12 -
6.13 /* content */
6.14
6.15 - {
6.16 - var t = first
6.17 - while (t != null) {
6.18 - t.command = this
6.19 - t = if (t == last) null else t.next
6.20 - }
6.21 - }
6.22 -
6.23 override def toString = name
6.24
6.25 - val name = text.content(first.start, first.stop)
6.26 - val content = text.content(proper_start, proper_stop)
6.27 + val name = tokens.head.content
6.28 + val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
6.29
6.30 - def next = if (last.next != null) last.next.command else null
6.31 - def prev = if (first.prev != null) first.prev.command else null
6.32 -
6.33 - def start = first.start
6.34 - def stop = last.stop
6.35 -
6.36 - def proper_start = start
6.37 - def proper_stop = {
6.38 - var i = last
6.39 - while (i != first && i.kind == Token.Kind.COMMENT)
6.40 - i = i.prev
6.41 - i.stop
6.42 - }
6.43 -
6.44 + def start = tokens.first.start
6.45 + def stop = tokens.last.stop
6.46
6.47 /* command status */
6.48
7.1 --- a/src/Tools/jEdit/src/prover/Prover.scala Thu Feb 05 21:18:30 2009 +0100
7.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Feb 19 20:44:28 2009 +0100
7.3 @@ -195,23 +195,19 @@
7.4 this.document = new ProofDocument(text, command_decls.contains(_))
7.5 process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
7.6
7.7 - document.structural_changes += (changes => {
7.8 + document.structural_changes += (changes => if(initialized){
7.9 for (cmd <- changes.removed_commands) remove(cmd)
7.10 - for (cmd <- changes.added_commands) send(cmd)
7.11 + changes.added_commands.foldLeft (changes.before_change) ((p, c) => {send(p, c); Some(c)})
7.12 })
7.13 - if (initialized) {
7.14 - document.activate()
7.15 - activated.event(())
7.16 - }
7.17 }
7.18
7.19 - private def send(cmd: Command) {
7.20 + private def send(prev: Option[Command], cmd: Command) {
7.21 cmd.status = Command.Status.UNPROCESSED
7.22 commands.put(cmd.id, cmd)
7.23
7.24 val content = isabelle_system.symbols.encode(cmd.content)
7.25 process.create_command(cmd.id, content)
7.26 - process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
7.27 + process.insert_command(prev match {case Some(c) => c.id case None => ""}, cmd.id)
7.28 }
7.29
7.30 def remove(cmd: Command) {