# HG changeset patch
# User wenzelm
# Date 1396792262 -7200
# Node ID b14bd153a7537849755d849b991952d4baf15a26
# Parent  30ccec1e82fb8884ebe3b3669b92d4739559df85
clarified position: no offset here;

diff -r 30ccec1e82fb -r b14bd153a753 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Apr 06 15:43:45 2014 +0200
+++ b/src/Pure/General/position.ML	Sun Apr 06 15:51:02 2014 +0200
@@ -20,8 +20,9 @@
   val file_name: string -> Properties.T
   val file_only: string -> T
   val file: string -> T
+  val line_file_only: int -> string -> T
+  val line_file: int -> string -> T
   val line: int -> T
-  val line_file: int -> string -> T
   val id: string -> T
   val id_only: string -> T
   val get_id: T -> string option
@@ -117,6 +118,7 @@
 fun file_only name = Pos ((0, 0, 0), file_name name);
 fun file name = Pos ((1, 1, 0), file_name name);
 
+fun line_file_only i name = Pos ((i, 0, 0), file_name name);
 fun line_file i name = Pos ((i, 1, 0), file_name name);
 fun line i = line_file i "";
 
diff -r 30ccec1e82fb -r b14bd153a753 src/Pure/ML-Systems/ml_positions.ML
--- a/src/Pure/ML-Systems/ml_positions.ML	Sun Apr 06 15:43:45 2014 +0200
+++ b/src/Pure/ML-Systems/ml_positions.ML	Sun Apr 06 15:51:02 2014 +0200
@@ -7,7 +7,7 @@
 fun ml_positions start_line name txt =
   let
     fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
-          let val s = "(Position.line_file " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
           in positions line cs (s :: res) end
       | positions line (c :: cs) res =
           positions (if c = #"\n" then line + 1 else line) cs (str c :: res)