location_of_position: Position.column_of (which counts Isabelle symbols, not characters);
authorwenzelm
Mon, 28 Jan 2008 22:27:26 +0100
changeset 26005 431ab3907291
parent 26004 2abb3005660f
child 26006 c973b4981276
location_of_position: Position.column_of (which counts Isabelle symbols, not characters);
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