clarified names: "peek" usually refers to evolving mutable state;

--- 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)