# HG changeset patch
# User wenzelm
# Date 1659605380 -7200
# Node ID 45fc58d48e4a459cf3320c13f856b8461a0d7ca8
# Parent  b6d74c90b58876b917f4d1ba461c8f0eec8300bb
tuned signature;

diff -r b6d74c90b588 -r 45fc58d48e4a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Aug 03 13:49:41 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 04 11:29:40 2022 +0200
@@ -59,7 +59,7 @@
   /* base info and source dependencies */
 
   sealed case class Base(
-    pos: Position.T = Position.none,
+    session_pos: Position.T = Position.none,
     session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
     proper_session_theories: List[Document.Node.Name] = Nil,
@@ -116,7 +116,7 @@
         (name, base) <- session_bases.iterator
         if base.errors.nonEmpty
       } yield cat_lines(base.errors) +
-          "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
+          "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.session_pos)
       ).toList
 
     def check_errors: Deps =
@@ -324,7 +324,7 @@
 
             val base =
               Base(
-                pos = info.pos,
+                session_pos = info.pos,
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
                 proper_session_theories = proper_session_theories,