# HG changeset patch # User wenzelm # Date 1672432077 -3600 # Node ID 72daee8a39cad989e75aee1835297e4bf3b9af07 # Parent 5ab016cbba18ace38a173e25138e759bcf9ec63b tuned signature: avoid too many aliases; diff -r 5ab016cbba18 -r 72daee8a39ca src/Pure/Admin/check_sources.scala --- a/src/Pure/Admin/check_sources.scala Fri Dec 30 21:09:50 2022 +0100 +++ b/src/Pure/Admin/check_sources.scala Fri Dec 30 21:27:57 2022 +0100 @@ -10,7 +10,7 @@ object Check_Sources { def check_file(path: Path): Unit = { val file_name = path.implode - val file_pos = path.position + val file_pos = Position.File(path.implode_symbolic) def line_pos(i: Int) = Position.Line_File(i + 1, file_name) if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux")) diff -r 5ab016cbba18 -r 72daee8a39ca src/Pure/General/path.scala --- a/src/Pure/General/path.scala Fri Dec 30 21:09:50 2022 +0100 +++ b/src/Pure/General/path.scala Fri Dec 30 21:27:57 2022 +0100 @@ -312,8 +312,6 @@ } catch { case ERROR(_) => None }).headOption.getOrElse(implode) } - def position: Position.T = Position.File(implode_symbolic) - /* platform files */