# HG changeset patch
# User wenzelm
# Date 1345829744 -7200
# Node ID 6f3ccfa7818dcb3c94d3d81a001f70518970333f
# Parent  5d8d409b897e2b3e91d7a598d3e0a731119c10df
more precise counting of line/column;

diff -r 5d8d409b897e -r 6f3ccfa7818d src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Aug 24 16:45:55 2012 +0200
+++ b/src/Pure/General/symbol.scala	Fri Aug 24 19:35:44 2012 +0200
@@ -8,6 +8,7 @@
 
 import scala.collection.mutable
 import scala.util.matching.Regex
+import scala.annotation.tailrec
 
 
 object Symbol
@@ -97,6 +98,16 @@
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
+  def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
+  {
+    var (line, column) = pos
+    for (sym <- iterator(text)) {
+      if (is_physical_newline(sym)) { line += 1; column = 1 }
+      else column += 1
+    }
+    (line, column)
+  }
+
 
   /* decoding offsets */
 
@@ -121,7 +132,7 @@
     {
       val sym = sym1 - 1
       val end = index.length
-      def bisect(a: Int, b: Int): Int =
+      @tailrec def bisect(a: Int, b: Int): Int =
       {
         if (a < b) {
           val c = (a + b) / 2
diff -r 5d8d409b897e -r 6f3ccfa7818d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 24 16:45:55 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 24 19:35:44 2012 +0200
@@ -153,10 +153,6 @@
 
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
 
-  val newlines =
-    (0 /: Symbol.iterator(source)) {
-      case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
-
   lazy val symbol_index = new Symbol.Index(source)
   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
diff -r 5d8d409b897e -r 6f3ccfa7818d src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 24 16:45:55 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 24 19:35:44 2012 +0200
@@ -131,25 +131,16 @@
                   case None => links
                 }
 
-              case Position.Id_Offset(def_id, def_offset) if !snapshot.is_outdated =>
-                snapshot.state.find_command(snapshot.version, def_id) match {
-                  case Some((def_node, def_cmd)) =>
-                    val file = new JFile(def_cmd.node_name.node)
+              case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
+                snapshot.state.find_command(snapshot.version, id) match {
+                  case Some((node, command)) =>
+                    val file = new JFile(command.node_name.node)
 
-                    // FIXME move!?
                     val sources =
-                      def_node.commands.iterator.takeWhile(_ != def_cmd).map(_.source) ++
-                        Iterator.single(def_cmd.source(Text.Range(0, def_offset)))
-                    var line = 1
-                    var column = 1
-                    for (source <- sources) {
-                      val newlines = (0 /: source.iterator) {  // FIXME Symbol.iterator!?
-                        case (n, c) => if (c == '\n') n + 1 else n }
-                      if (newlines > 0) {
-                        line += newlines
-                        column = source.lastIndexOf('\n') + 2
-                      }
-                    }
+                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
+                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+
                     Text.Info(snapshot.convert(info_range), Hyperlink(file, line, column)) :: links
 
                   case None => links