# 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)