tuned signature: avoid too many aliases;
authorwenzelm
Fri, 30 Dec 2022 21:27:57 +0100
changeset 76831 72daee8a39ca
parent 76830 5ab016cbba18
child 76833 6be3459fc4c1
child 76839 2121fde115b2
tuned signature: avoid too many aliases;
src/Pure/Admin/check_sources.scala
src/Pure/General/path.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"))
--- 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 */