# HG changeset patch
# User wenzelm
# Date 1660307177 -7200
# Node ID e71fbea76bd96526847bb124a11a5b5181e56f2b
# Parent  b702a015fb22bdcb9144470958e3896710c164b8
unused (see 696819fe2424);

diff -r b702a015fb22 -r e71fbea76bd9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 12 13:16:02 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 12 14:26:17 2022 +0200
@@ -78,9 +78,6 @@
       abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil
     ) {
-      def imports_offset: Map[Int, Name] =
-        (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap
-
       def imports: List[Name] = imports_pos.map(_._1)
 
       def append_errors(msgs: List[String]): Header =