# HG changeset patch
# User wenzelm
# Date 1201555646 -3600
# Node ID 431ab3907291487bf79f1809a8551578335beada
# Parent  2abb3005660f160529ac9f3b67dfac749255154c
location_of_position: Position.column_of (which counts Isabelle symbols, not characters);

diff -r 2abb3005660f -r 431ab3907291 src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon Jan 28 22:27:24 2008 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon Jan 28 22:27:26 2008 +0100
@@ -75,6 +75,7 @@
 
 fun location_of_position pos =
     let val line = Position.line_of pos
+        val column = Position.column_of pos
         val (url,descr) =
             (case Position.file_of pos of
                NONE => (NONE, NONE)
@@ -85,7 +86,7 @@
                  | NONE => (NONE, SOME fname)
                end);
     in
-        { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
+        { descr=descr, url=url, line=line, column=column, char=NONE, length=NONE }
     end