tuned signature;
authorwenzelm
Wed Aug 29 19:35:41 2018 +0200 (13 months ago)
changeset 68846da0cb00a4d6a
parent 68845 3b2daa7bf9f4
child 68847 511d163ab623
tuned signature;
src/Pure/Thy/thy_element.scala
     1.1 --- a/src/Pure/Thy/thy_element.scala	Wed Aug 29 18:53:58 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_element.scala	Wed Aug 29 19:35:41 2018 +0200
     1.3 @@ -24,6 +24,12 @@
     1.4            b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed)
     1.5          } yield b)
     1.6  
     1.7 +    def outline_iterator: Iterator[A] =
     1.8 +      proof match {
     1.9 +        case None => Iterator(head)
    1.10 +        case Some((_, qed)) => Iterator(head, qed)
    1.11 +      }
    1.12 +
    1.13      def last: A =
    1.14        proof match {
    1.15          case None => head
    1.16 @@ -37,7 +43,9 @@
    1.17  
    1.18    /* parse elements */
    1.19  
    1.20 -  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element[Command]] =
    1.21 +  type Element_Command = Element[Command]
    1.22 +
    1.23 +  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element_Command] =
    1.24    {
    1.25      case class Reader(in: List[Command]) extends input.Reader[Command]
    1.26      {
    1.27 @@ -67,17 +75,17 @@
    1.28        def category(pred: String => Boolean, other: Boolean): Parser[Command] =
    1.29          command(_.span.is_kind(keywords, pred, other))
    1.30  
    1.31 -      def theory_element: Parser[Element[Command]] =
    1.32 +      def theory_element: Parser[Element_Command] =
    1.33          category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
    1.34 -      def proof_element: Parser[Element[Command]] =
    1.35 +      def proof_element: Parser[Element_Command] =
    1.36          category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } |
    1.37          category(Keyword.proof_body, true) ^^ { case a => atom(a) }
    1.38        def proof: Parser[Proof[Command]] =
    1.39          rep(proof_element) ~ category(Keyword.qed, false) ^^ { case a ~ b => (a, b) }
    1.40  
    1.41 -      val default_element: Parser[Element[Command]] = command(_ => true) ^^ { case a => atom(a) }
    1.42 +      val default_element: Parser[Element_Command] = command(_ => true) ^^ { case a => atom(a) }
    1.43  
    1.44 -      def apply: List[Element[Command]] =
    1.45 +      def apply: List[Element_Command] =
    1.46          rep(theory_element | default_element)(Reader(commands)) match {
    1.47            case Success(result, rest) if rest.atEnd => result
    1.48            case bad => error(bad.toString)