clarified names;
authorwenzelm
Sat, 30 Jul 2022 13:53:15 +0200
changeset 75729 20a03e16d8fa
parent 75728 3f64fdf75082
child 75730 6f46853dbec4
clarified names;
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)
   }