# HG changeset patch
# User wenzelm
# Date 1393847652 -3600
# Node ID f2c0eaedd579fbd215d763b381d58b7e380fb9c7
# Parent  6f50d445f0e37109d4b68cc9333b40c2c5d5bc2c
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);

diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Pure/General/position.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -50,8 +50,8 @@
 
   object Range
   {
-    def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop)
-    def unapply(pos: T): Option[Text.Range] =
+    def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop)
+    def unapply(pos: T): Option[Symbol.Range] =
       (pos, pos) match {
         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
         case (Offset(start), _) => Some(Text.Range(start, start + 1))
@@ -61,7 +61,7 @@
 
   object Id_Offset
   {
-    def unapply(pos: T): Option[(Long, Text.Offset)] =
+    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
       (pos, pos) match {
         case (Id(id), Offset(offset)) => Some((id, offset))
         case _ => None
@@ -70,7 +70,7 @@
 
   object Def_Id_Offset
   {
-    def unapply(pos: T): Option[(Long, Text.Offset)] =
+    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
       (pos, pos) match {
         case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
         case _ => None
@@ -79,7 +79,7 @@
 
   object Reported
   {
-    def unapply(pos: T): Option[(Long, String, Text.Range)] =
+    def unapply(pos: T): Option[(Long, String, Symbol.Range)] =
       (pos, pos) match {
         case (Id(id), Range(range)) =>
           Some((id, File.unapply(pos).getOrElse(""), range))
diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Pure/General/symbol.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -16,6 +16,10 @@
 {
   type Symbol = String
 
+  // counting Isabelle symbols, starting from 1
+  type Offset = Text.Offset
+  type Range = Text.Range
+
 
   /* ASCII characters */
 
@@ -142,9 +146,9 @@
       buf.toArray
     }
 
-    def decode(sym1: Int): Int =
+    def decode(symbol_offset: Offset): Text.Offset =
     {
-      val sym = sym1 - 1
+      val sym = symbol_offset - 1
       val end = index.length
       @tailrec def bisect(a: Int, b: Int): Int =
       {
@@ -160,7 +164,7 @@
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
-    def decode(range: Text.Range): Text.Range = range.map(decode(_))
+    def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
   }
 
 
diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -152,11 +152,12 @@
               def bad(): Unit = System.err.println("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
+                case XML.Elem(Markup(name,
+                  atts @ Position.Reported(id, file_name, symbol_range)), args)
                 if id == command.id || id == alt_id =>
                   command.chunks.get(file_name) match {
                     case Some(chunk) =>
-                      chunk.incorporate(raw_range) match {
+                      chunk.incorporate(symbol_range) match {
                         case Some(range) =>
                           val props = Position.purge(atts)
                           val info = Text.Info(range, XML.Elem(Markup(name, props), args))
@@ -216,16 +217,16 @@
     def file_name: String
     def length: Int
     def range: Text.Range
-    def decode(raw_range: Text.Range): Text.Range
+    def decode(symbol_range: Symbol.Range): Text.Range
 
-    def incorporate(raw_range: Text.Range): Option[Text.Range] =
+    def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
     {
-      def inc(r: Text.Range): Option[Text.Range] =
+      def inc(r: Symbol.Range): Option[Text.Range] =
         range.try_restrict(decode(r)) match {
           case Some(r1) if !r1.is_singularity => Some(r1)
           case _ => None
         }
-     inc(raw_range) orElse inc(raw_range - 1)
+     inc(symbol_range) orElse inc(symbol_range - 1)
     }
   }
 
@@ -234,7 +235,7 @@
     val length = text.length
     val range = Text.Range(0, length)
     private val symbol_index = Symbol.Index(text)
-    def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
+    def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
 
     override def toString: String = "Command.File(" + file_name + ")"
   }
@@ -374,8 +375,8 @@
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
 
   private lazy val symbol_index = Symbol.Index(source)
-  def decode(raw_offset: Text.Offset): Text.Offset = symbol_index.decode(raw_offset)
-  def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
+  def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
+  def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
 
 
   /* accumulated results */
diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -24,6 +24,6 @@
 
   abstract class Hyperlink { def follow(context: Context): Unit }
   def hyperlink_command(
-    snapshot: Document.Snapshot, command: Command, raw_offset: Text.Offset = 0): Option[Hyperlink]
+    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
 }
 
diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -287,9 +287,9 @@
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, file_name, raw_range)
+        case Position.Reported(id, file_name, symbol_range)
         if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
-          chunk.incorporate(raw_range) match {
+          chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set
           }
diff -r 6f50d445f0e3 -r f2c0eaedd579 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 12:24:14 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 12:54:12 2014 +0100
@@ -145,8 +145,8 @@
 
   /* hyperlinks */
 
-  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
-    : Option[Hyperlink] =
+  override def hyperlink_command(
+    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
   {
     if (snapshot.is_outdated) None
     else {
@@ -156,8 +156,8 @@
           val file_name = command.node_name.node
           val sources =
             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-              (if (raw_offset == 0) Iterator.empty
-               else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
+              (if (offset == 0) Iterator.empty
+               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
           val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
           Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
       }
@@ -167,10 +167,10 @@
   def hyperlink_command_id(
     snapshot: Document.Snapshot,
     id: Document_ID.Generic,
-    raw_offset: Text.Offset): Option[Hyperlink] =
+    offset: Symbol.Offset): Option[Hyperlink] =
   {
     snapshot.state.find_command(snapshot.version, id) match {
-      case Some((node, command)) => hyperlink_command(snapshot, command, raw_offset)
+      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
       case None => None
     }
   }
@@ -178,7 +178,7 @@
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
 
-  def hyperlink_source_file(source_name: String, line: Int, raw_offset: Text.Offset)
+  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
     : Option[Hyperlink] =
   {
     if (Path.is_valid(source_name)) {
@@ -186,12 +186,12 @@
         case Some(path) =>
           val name = Isabelle_System.platform_path(path)
           JEdit_Lib.jedit_buffer(name) match {
-            case Some(buffer) if raw_offset > 0 =>
+            case Some(buffer) if offset > 0 =>
               val (line, column) =
                 JEdit_Lib.buffer_lock(buffer) {
                   ((1, 1) /:
                     (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                      zipWithIndex.takeWhile(p => p._2 < raw_offset - 1).map(_._1)))(
+                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
                         Symbol.advance_line_column)
                 }
               Some(hyperlink_file(name, line, column))