# HG changeset patch
# User wenzelm
# Date 1659181995 -7200
# Node ID 20a03e16d8fae382775df5935402691e7c30f8a1
# Parent  3f64fdf750823364b8a41d7027f689d465ac6bdd
clarified names;

diff -r 3f64fdf75082 -r 20a03e16d8fa src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Jul 30 13:44:26 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Jul 30 13:53:15 2022 +0200
@@ -110,9 +110,9 @@
     val empty: Nodes = make(Nil)
     def make(infos: Iterable[(String, Node_Info)]): Nodes = new Nodes(infos.toMap)
   }
-  class Nodes private(by_session: Map[String, Node_Info]) {
-    def apply(name: String): Node_Info = by_session.getOrElse(name, Node_Info.empty)
-    def get(name: String): Option[Node_Info] = by_session.get(name)
+  class Nodes private(theory_node_info: Map[String, Node_Info]) {
+    def apply(name: String): Node_Info = theory_node_info.getOrElse(name, Node_Info.empty)
+    def get(name: String): Option[Node_Info] = theory_node_info.get(name)
   }