1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Jan 10 17:10:32 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Jan 10 20:14:21 2010 +0100
     1.3 @@ -126,31 +126,27 @@
     1.4      {
     1.5        def from_current(pos: Int) = model.from_current(document, pos)
     1.6        def to_current(pos: Int) = model.to_current(document, pos)
     1.7 +      val metrics = text_area.getPainter.getFontMetrics
     1.8        val saved_color = gfx.getColor
     1.9 -
    1.10 -      val metrics = text_area.getPainter.getFontMetrics
    1.11 -
    1.12 -      // encolor phase
    1.13 -      var cmd = document.command_at(from_current(start))
    1.14 -      while (cmd.isDefined && cmd.get.start(document) < end) {
    1.15 -        val e = cmd.get
    1.16 -        val begin = start max to_current(e.start(document))
    1.17 -        val finish = (end - 1) min to_current(e.stop(document))
    1.18 -        encolor(gfx, y, metrics.getHeight, begin, finish,
    1.19 -          Document_View.choose_color(e, document), true)
    1.20 -        cmd = document.commands.next(e)
    1.21 +      try {
    1.22 +        for ((command, command_start) <-
    1.23 +          document.command_range(from_current(start), from_current(end)))
    1.24 +        {
    1.25 +          val begin = start max to_current(command_start)
    1.26 +          val finish = (end - 1) min to_current(command_start + command.length)
    1.27 +          encolor(gfx, y, metrics.getHeight, begin, finish,
    1.28 +            Document_View.choose_color(command, document), true)
    1.29 +        }
    1.30        }
    1.31 -
    1.32 -      gfx.setColor(saved_color)
    1.33 +      finally { gfx.setColor(saved_color) }
    1.34      }
    1.35  
    1.36      override def getToolTipText(x: Int, y: Int): String =
    1.37      {
    1.38        val offset = model.from_current(document, text_area.xyToOffset(x, y))
    1.39        document.command_at(offset) match {
    1.40 -        case Some(cmd) =>
    1.41 -          document.token_start(cmd.tokens.first)
    1.42 -          document.current_state(cmd).type_at(offset - cmd.start(document)).getOrElse(null)
    1.43 +        case Some((command, command_start)) =>
    1.44 +          document.current_state(command).type_at(offset - command_start).getOrElse(null)
    1.45          case None => null
    1.46        }
    1.47      }
    1.48 @@ -169,12 +165,11 @@
    1.49  
    1.50    private val caret_listener = new CaretListener
    1.51    {
    1.52 -    override def caretUpdate(e: CaretEvent) {
    1.53 +    override def caretUpdate(e: CaretEvent)
    1.54 +    {
    1.55        document.command_at(e.getDot) match {
    1.56 -        case Some(cmd)
    1.57 -          if (document.token_start(cmd.tokens.first) <= e.getDot &&
    1.58 -            selected_command != cmd) =>
    1.59 -          selected_command = cmd  // FIXME !?
    1.60 +        case Some((command, command_start)) if (selected_command != command) =>
    1.61 +          selected_command = command
    1.62          case _ =>
    1.63        }
    1.64      }

     2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Jan 10 17:10:32 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Jan 10 20:14:21 2010 +0100
     2.3 @@ -44,10 +44,9 @@
     2.4          val document = model.recent_document()
     2.5          val offset = model.from_current(document, original_offset)
     2.6          document.command_at(offset) match {
     2.7 -          case Some(command) =>
     2.8 -            document.current_state(command).ref_at(offset - command.start(document)) match {
     2.9 +          case Some((command, command_start)) =>
    2.10 +            document.current_state(command).ref_at(offset - command_start) match {
    2.11                case Some(ref) =>
    2.12 -                val command_start = command.start(document)
    2.13                  val begin = model.to_current(document, command_start + ref.start)
    2.14                  val line = buffer.getLineOfOffset(begin)
    2.15                  val end = model.to_current(document, command_start + ref.stop)

     3.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun Jan 10 17:10:32 2010 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun Jan 10 20:14:21 2010 +0100
     3.3 @@ -115,37 +115,32 @@
     3.4      def from: Int => Int = model.from_current(document, _)
     3.5  
     3.6      var next_x = start
     3.7 -    var cmd = document.command_at(from(start))
     3.8 -    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
     3.9 -      val command = cmd.get
    3.10 -      for {
    3.11 -        markup <- document.current_state(command).highlight.flatten
    3.12 -        command_start = command.start(document)
    3.13 -        abs_start = to(command_start + markup.start)
    3.14 -        abs_stop = to(command_start + markup.stop)
    3.15 -        if (abs_stop > start)
    3.16 -        if (abs_start < stop)
    3.17 -        byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
    3.18 -        token_start = (abs_start - start) max 0
    3.19 -        token_length =
    3.20 -          (abs_stop - abs_start) -
    3.21 -          ((start - abs_start) max 0) -
    3.22 -          ((abs_stop - stop) max 0)
    3.23 -      } {
    3.24 +    for {
    3.25 +      (command, command_start) <- document.command_range(from(start), from(stop))
    3.26 +      markup <- document.current_state(command).highlight.flatten
    3.27 +      val abs_start = to(command_start + markup.start)
    3.28 +      val abs_stop = to(command_start + markup.stop)
    3.29 +      if (abs_stop > start)
    3.30 +      if (abs_start < stop)
    3.31 +      val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
    3.32 +      val token_start = (abs_start - start) max 0
    3.33 +      val token_length =
    3.34 +        (abs_stop - abs_start) -
    3.35 +        ((start - abs_start) max 0) -
    3.36 +        ((abs_stop - stop) max 0)
    3.37 +      }
    3.38 +      {
    3.39          if (start + token_start > next_x)
    3.40            handler.handleToken(line_segment, 1,
    3.41              next_x - start, start + token_start - next_x, context)
    3.42 -        handler.handleToken(line_segment, byte,
    3.43 -          token_start, token_length, context)
    3.44 +        handler.handleToken(line_segment, byte, token_start, token_length, context)
    3.45          next_x = start + token_start + token_length
    3.46        }
    3.47 -      cmd = document.commands.next(command)
    3.48 -    }
    3.49      if (next_x < stop)
    3.50        handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
    3.51  
    3.52      handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
    3.53      handler.setLineContext(context)
    3.54 -    return context
    3.55 +    context
    3.56    }
    3.57  }

     4.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Sun Jan 10 17:10:32 2010 +0100
     4.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Sun Jan 10 20:14:21 2010 +0100
     4.3 @@ -51,8 +51,10 @@
     4.4    def content(i: Int, j: Int): String = content.substring(i, j)
     4.5    lazy val symbol_index = new Symbol.Index(content)
     4.6  
     4.7 +  def length: Int = content.length
     4.8 +
     4.9    def start(doc: Document) = doc.token_start(tokens.first)
    4.10 -  def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length
    4.11 +  def stop(doc: Document) = start(doc) + length
    4.12  
    4.13    def contains(p: Token) = tokens.contains(p)
    4.14  

     5.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Sun Jan 10 17:10:32 2010 +0100
     5.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Sun Jan 10 20:14:21 2010 +0100
     5.3 @@ -245,6 +245,7 @@
     5.4    }
     5.5  }
     5.6  
     5.7 +
     5.8  class Document(
     5.9      val id: Isar_Document.Document_ID,
    5.10      val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
    5.11 @@ -252,10 +253,41 @@
    5.12      val commands: Linear_Set[Command],
    5.13      old_states: Map[Command, Command])
    5.14  {
    5.15 +  // FIXME eliminate
    5.16    def content = Token.string_from_tokens(Nil ++ tokens, token_start)
    5.17  
    5.18  
    5.19 -  /* command/state assignment */
    5.20 +  /* command source positions */
    5.21 +
    5.22 +  def command_starts: Iterator[(Command, Int)] =
    5.23 +  {
    5.24 +    var offset = 0
    5.25 +    for (cmd <- commands.elements) yield {
    5.26 +      // val start = offset  FIXME new
    5.27 +      val start = token_start(cmd.tokens.first)   // FIXME old
    5.28 +      offset += cmd.length
    5.29 +      (cmd, start)
    5.30 +    }
    5.31 +  }
    5.32 +
    5.33 +  def command_start(cmd: Command): Option[Int] =
    5.34 +    command_starts.find(_._1 == cmd).map(_._2)
    5.35 +
    5.36 +  def command_range(i: Int): Iterator[(Command, Int)] =
    5.37 +    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    5.38 +
    5.39 +  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
    5.40 +    command_range(i) takeWhile { case (_, start) => start < j }
    5.41 +
    5.42 +  def command_at(i: Int): Option[(Command, Int)] =
    5.43 +  {
    5.44 +    val range = command_range(i)
    5.45 +    if (range.hasNext) Some(range.next) else None
    5.46 +  }
    5.47 +
    5.48 +
    5.49 +
    5.50 +  /* command state assignment */
    5.51  
    5.52    val assignment = Future.promise[Map[Command, Command]]
    5.53    def await_assignment { assignment.join }
    5.54 @@ -273,33 +305,4 @@
    5.55      require(assignment.is_finished)
    5.56      (assignment.join)(cmd).current_state
    5.57    }
    5.58 -
    5.59 -
    5.60 -  val commands_offsets = {
    5.61 -    var last_stop = 0
    5.62 -    (for (c <- commands) yield {
    5.63 -      val r = c -> (last_stop, c.stop(this))
    5.64 -      last_stop = c.stop(this)
    5.65 -      r
    5.66 -    }).toArray
    5.67 -  }
    5.68 -
    5.69 -  def command_at(pos: Int): Option[Command] =
    5.70 -    find_command(pos, 0, commands_offsets.length)
    5.71 -
    5.72 -  // use a binary search to find commands for a given offset
    5.73 -  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
    5.74 -  {
    5.75 -    val middle_index = (array_start + array_stop) / 2
    5.76 -    if (middle_index >= commands_offsets.length) return None
    5.77 -    val (middle, (start, stop)) = commands_offsets(middle_index)
    5.78 -    // does middle contain pos?
    5.79 -    if (start <= pos && pos < stop)
    5.80 -      Some(middle)
    5.81 -    else if (start > pos)
    5.82 -      find_command(pos, array_start, middle_index)
    5.83 -    else if (stop <= pos)
    5.84 -      find_command(pos, middle_index + 1, array_stop)
    5.85 -    else error("impossible")
    5.86 -  }
    5.87  }