# HG changeset patch
# User wenzelm
# Date 1736693672 -3600
# Node ID bd24acc5162cd690fc7bc1d42ccd1473f2872de5
# Parent  3a0ef100c86ea72c32ba3e816d15227b22b2cf00
clarified names: "peek" usually refers to evolving mutable state;

diff -r 3a0ef100c86e -r bd24acc5162c src/Tools/Find_Facts/src/thy_blocks.scala
--- a/src/Tools/Find_Facts/src/thy_blocks.scala	Sun Jan 12 15:53:50 2025 +0100
+++ b/src/Tools/Find_Facts/src/thy_blocks.scala	Sun Jan 12 15:54:32 2025 +0100
@@ -75,7 +75,7 @@
     }
 
     case class Blocks(private val stack: List[Block], private val out: List[Block]) {
-      def peek: Option[Block] = stack.headOption
+      def top: Option[Block] = stack.headOption
       def push(block: Block): Blocks = copy(stack = block :: stack)
       def add(block: Block): Blocks =
         stack match {
@@ -110,7 +110,7 @@
 
     def parse(spans: List[Span]): List[Block] = {
       def parse1(blocks: Blocks, span: Span): Blocks =
-        blocks.peek match {
+        blocks.top match {
           case _ if span.is_of_kind(Keyword.document) => blocks.add(span)
           case None if span.is_of_kind(Keyword.theory_begin) => blocks.push(Thy(List(span)))
           case Some(_) if span.is_of_kind(Keyword.diag) => blocks.add(span)