# HG changeset patch # User wenzelm # Date 1514371898 -3600 # Node ID dfc5a150391648fb2a75192efe8468908030317c # Parent d327c11c9f3e7f82e6640a1299aab617a9d4b536 clarified default position for empty message pos; diff -r d327c11c9f3e -r dfc5a1503916 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Mon Dec 25 11:22:49 2017 +0100 +++ b/src/Pure/General/position.ML Wed Dec 27 11:51:38 2017 +0100 @@ -24,6 +24,7 @@ val line_file_only: int -> string -> T val line_file: int -> string -> T val line: int -> T + val get_props: T -> Properties.T val id: string -> T val id_only: string -> T val get_id: T -> string option @@ -131,6 +132,8 @@ fun line_file i name = Pos ((i, 1, 0), file_name name); fun line i = line_file i ""; +fun get_props (Pos (_, props)) = props; + fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]); fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]); diff -r d327c11c9f3e -r dfc5a1503916 src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML Mon Dec 25 11:22:49 2017 +0100 +++ b/src/Pure/Thy/bibtex.ML Wed Dec 27 11:51:38 2017 +0100 @@ -24,8 +24,7 @@ |> YXML.parse_body |> let open XML.Decode in list (triple bool string properties) end |> map (fn (is_error, msg, pos) => - {is_error = is_error, msg = msg, - pos = Position.of_properties (pos @ Position.properties_of pos0)}); + {is_error = is_error, msg = msg, pos = Position.of_properties (pos @ Position.get_props pos0)}); fun check_database_output pos0 database = let