# HG changeset patch
# User wenzelm
# Date 1535564141 -7200
# Node ID da0cb00a4d6a9a6b4c72b19fb3ee0db454259f09
# Parent  3b2daa7bf9f4a94ab9ff522c1b99eb78bc9df159
tuned signature;

diff -r 3b2daa7bf9f4 -r da0cb00a4d6a src/Pure/Thy/thy_element.scala
--- a/src/Pure/Thy/thy_element.scala	Wed Aug 29 18:53:58 2018 +0200
+++ b/src/Pure/Thy/thy_element.scala	Wed Aug 29 19:35:41 2018 +0200
@@ -24,6 +24,12 @@
           b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed)
         } yield b)
 
+    def outline_iterator: Iterator[A] =
+      proof match {
+        case None => Iterator(head)
+        case Some((_, qed)) => Iterator(head, qed)
+      }
+
     def last: A =
       proof match {
         case None => head
@@ -37,7 +43,9 @@
 
   /* parse elements */
 
-  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element[Command]] =
+  type Element_Command = Element[Command]
+
+  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] =
   {
     case class Reader(in: List[Command]) extends input.Reader[Command]
     {
@@ -67,17 +75,17 @@
       def category(pred: String => Boolean, other: Boolean): Parser[Command] =
         command(_.span.is_kind(keywords, pred, other))
 
-      def theory_element: Parser[Element[Command]] =
+      def theory_element: Parser[Element_Command] =
         category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
-      def proof_element: Parser[Element[Command]] =
+      def proof_element: Parser[Element_Command] =
         category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } |
         category(Keyword.proof_body, true) ^^ { case a => atom(a) }
       def proof: Parser[Proof[Command]] =
         rep(proof_element) ~ category(Keyword.qed, false) ^^ { case a ~ b => (a, b) }
 
-      val default_element: Parser[Element[Command]] = command(_ => true) ^^ { case a => atom(a) }
+      val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) }
 
-      def apply: List[Element[Command]] =
+      def apply: List[Element_Command] =
         rep(theory_element | default_element)(Reader(commands)) match {
           case Success(result, rest) if rest.atEnd => result
           case bad => error(bad.toString)