--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Sun Sep 06 14:55:25 2009 +0200
@@ -121,9 +121,10 @@
def to: Int => Int = theory_view.to_current(document, _)
def from: Int => Int = theory_view.from_current(document, _)
- var command = document.find_command_at(from(start))
var next_x = start
- while (command != null && command.start(document) < from(stop)) {
+ var cmd = document.command_at(from(start))
+ while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
+ val command = cmd.get
for {
markup <- command.highlight_node(document).flatten
command_start = command.start(document)
@@ -145,7 +146,7 @@
token_start, token_length, context)
next_x = start + token_start + token_length
}
- command = document.commands.next(command).getOrElse(null)
+ cmd = document.commands.next(command)
}
if (next_x < stop)
handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Sun Sep 06 14:55:25 2009 +0200
@@ -51,30 +51,30 @@
val theory_view = theory_view_opt.get
val document = theory_view.current_document()
val offset = theory_view.from_current(document, original_offset)
- val command = document.find_command_at(offset)
- if (command != null) {
- val ref_o = command.ref_at(document, offset - command.start(document))
- if (!ref_o.isDefined) null
- else {
- val ref = ref_o.get
- val command_start = command.start(document)
- val begin = theory_view.to_current(document, command_start + ref.start)
- val line = buffer.getLineOfOffset(begin)
- val end = theory_view.to_current(document, command_start + ref.stop)
- ref.info match {
- case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
- new ExternalHyperlink(begin, end, line, ref_file, ref_line)
- case Command.RefInfo(_, _, Some(id), Some(offset)) =>
- prover.get.command(id) match {
- case Some(ref_cmd) =>
- new InternalHyperlink(begin, end, line,
- theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+ document.command_at(offset) match {
+ case Some(command) =>
+ command.ref_at(document, offset - command.start(document)) match {
+ case Some(ref) =>
+ val command_start = command.start(document)
+ val begin = theory_view.to_current(document, command_start + ref.start)
+ val line = buffer.getLineOfOffset(begin)
+ val end = theory_view.to_current(document, command_start + ref.stop)
+ ref.info match {
+ case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+ new ExternalHyperlink(begin, end, line, ref_file, ref_line)
+ case Command.RefInfo(_, _, Some(id), Some(offset)) =>
+ prover.get.command(id) match {
+ case Some(ref_cmd) =>
+ new InternalHyperlink(begin, end, line,
+ theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+ case None => null
+ }
case _ => null
}
- case _ => null
+ case None => null
}
- }
- } else null
+ case None => null
+ }
}
}
}
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Sep 06 14:55:25 2009 +0200
@@ -54,10 +54,13 @@
private val selected_state_controller = new CaretListener {
override def caretUpdate(e: CaretEvent) = {
val doc = current_document()
- val cmd = doc.find_command_at(e.getDot)
- if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
- Isabelle.plugin.selected_state != cmd)
- Isabelle.plugin.selected_state = cmd
+ doc.command_at(e.getDot) match {
+ case Some(cmd)
+ if (doc.token_start(cmd.tokens.first) <= e.getDot &&
+ Isabelle.plugin.selected_state != cmd) =>
+ Isabelle.plugin.selected_state = cmd
+ case _ =>
+ }
}
}
@@ -270,13 +273,14 @@
val metrics = text_area.getPainter.getFontMetrics
// encolor phase
- var e = document.find_command_at(from_current(start))
- while (e != null && e.start(document) < end) {
+ var cmd = document.command_at(from_current(start))
+ while (cmd.isDefined && cmd.get.start(document) < end) {
+ val e = cmd.get
val begin = start max to_current(e.start(document))
val finish = (end - 1) min to_current(e.stop(document))
encolor(gfx, y, metrics.getHeight, begin, finish,
TheoryView.choose_color(e, document), true)
- e = document.commands.next(e).getOrElse(null)
+ cmd = document.commands.next(e)
}
gfx.setColor(saved_color)
@@ -286,11 +290,12 @@
{
val document = current_document()
val offset = from_current(document, text_area.xyToOffset(x, y))
- val cmd = document.find_command_at(offset)
- if (cmd != null) {
- document.token_start(cmd.tokens.first)
- cmd.type_at(document, offset - cmd.start(document))
- } else null
+ document.command_at(offset) match {
+ case Some(cmd) =>
+ document.token_start(cmd.tokens.first)
+ cmd.type_at(document, offset - cmd.start(document))
+ case None => null
+ }
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Sep 06 13:43:54 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Sep 06 14:55:25 2009 +0200
@@ -260,20 +260,22 @@
}).toArray
}
+ def command_at(pos: Int): Option[Command] =
+ find_command(pos, 0, commands_offsets.length)
+
// use a binary search to find commands for a given offset
- def find_command_at(pos: Int): Command = find_command_at(pos, 0, commands_offsets.length)
- private def find_command_at(pos: Int, array_start: Int, array_stop: Int): Command = {
+ private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
+ {
val middle_index = (array_start + array_stop) / 2
- if (middle_index >= commands_offsets.length) return null
+ if (middle_index >= commands_offsets.length) return None
val (middle, (start, stop)) = commands_offsets(middle_index)
// does middle contain pos?
- if (start <= pos && stop > pos)
- middle
+ if (start <= pos && pos < stop)
+ Some(middle)
else if (start > pos)
- find_command_at(pos, array_start, middle_index)
+ find_command(pos, array_start, middle_index)
else if (stop <= pos)
- find_command_at(pos, middle_index + 1, array_stop)
- else error("can't be")
+ find_command(pos, middle_index + 1, array_stop)
+ else error("impossible")
}
-
}