# HG changeset patch
# User wenzelm
# Date 1282123509 -7200
# Node ID d72479a078822ff4a9822bfc380d643fc518da20
# Parent  1dd4f545ac24e559552b8a0294f7c5a9f7e6ffe5
decode Isabelle symbol positions in one spot;

diff -r 1dd4f545ac24 -r d72479a07882 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 18 11:08:28 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Aug 18 11:25:09 2010 +0200
@@ -92,14 +92,14 @@
                     if (kind == Markup.ML_TYPING) {
                       val info = Pretty.string_of(body, margin = 40)
                       state.add_markup(
-                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+                        command.markup_node(begin, end, Command.TypeInfo(info)))
                     }
                     else if (kind == Markup.ML_REF) {
                       body match {
                         case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
                           state.add_markup(
                             command.markup_node(
-                              begin - 1, end - 1,
+                              begin, end,
                               Command.RefInfo(
                                 Position.get_file(props),
                                 Position.get_line(props),
@@ -110,7 +110,7 @@
                     }
                     else {
                       state.add_markup(
-                        command.markup_node(begin - 1, end - 1,
+                        command.markup_node(begin, end,
                           Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
                     }
                   case _ => state
@@ -159,8 +159,8 @@
 
   def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   {
-    val start = symbol_index.decode(begin)
-    val stop = symbol_index.decode(end)
+    val start = symbol_index.decode(begin - 1)
+    val stop = symbol_index.decode(end - 1)
     new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
   }