# HG changeset patch
# User wenzelm
# Date 1535561638 -7200
# Node ID 3b2daa7bf9f4a94ab9ff522c1b99eb78bc9df159
# Parent  63c9c6ceb7a31f8ad7933c458bdbaa06c19f2820
support Thy_Element in Scala, following ML version;

diff -r 63c9c6ceb7a3 -r 3b2daa7bf9f4 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Wed Aug 29 18:53:29 2018 +0200
+++ b/src/Pure/Isar/document_structure.scala	Wed Aug 29 18:53:58 2018 +0200
@@ -21,7 +21,8 @@
   case class Atom(length: Int) extends Document
 
   private def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
-    command.span.is_kind(keywords, kind => Keyword.theory(kind) && !Keyword.theory_end(kind))
+    command.span.is_kind(keywords,
+      kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
 
 
 
diff -r 63c9c6ceb7a3 -r 3b2daa7bf9f4 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Wed Aug 29 18:53:29 2018 +0200
+++ b/src/Pure/PIDE/command_span.scala	Wed Aug 29 18:53:58 2018 +0200
@@ -39,10 +39,10 @@
         case _ => start
       }
 
-    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
+    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
       keywords.kinds.get(name) match {
         case Some(k) => pred(k)
-        case None => false
+        case None => other
       }
 
     def is_begin: Boolean = content.exists(_.is_begin)
diff -r 63c9c6ceb7a3 -r 3b2daa7bf9f4 src/Pure/Thy/thy_element.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_element.scala	Wed Aug 29 18:53:58 2018 +0200
@@ -0,0 +1,88 @@
+/*  Title:      Pure/Thy/thy_element.ML
+    Author:     Makarius
+
+Theory elements: statements with optional proof.
+*/
+
+package isabelle
+
+import scala.util.parsing.combinator.Parsers
+import scala.util.parsing.input
+
+
+object Thy_Element
+{
+  /* datatype element */
+
+  type Proof[A] = (List[Element[A]], A)
+  sealed case class Element[A](head: A, proof: Option[Proof[A]])
+  {
+    def iterator: Iterator[A] =
+      Iterator(head) ++
+        (for {
+          (prf, qed) <- proof.iterator
+          b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed)
+        } yield b)
+
+    def last: A =
+      proof match {
+        case None => head
+        case Some((_, qed)) => qed
+      }
+  }
+
+  def element[A](a: A, b: Proof[A]): Element[A] = Element(a, Some(b))
+  def atom[A](a: A): Element[A] = Element(a, None)
+
+
+  /* parse elements */
+
+  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element[Command]] =
+  {
+    case class Reader(in: List[Command]) extends input.Reader[Command]
+    {
+      def first: Command = in.head
+      def rest: Reader = Reader(in.tail)
+      def pos: input.Position = input.NoPosition
+      def atEnd: Boolean = in.isEmpty
+    }
+
+    object Parser extends Parsers
+    {
+      type Elem = Command
+
+      def command(pred: Command => Boolean): Parser[Command] =
+        new Parser[Elem] {
+          def apply(in: Input) =
+          {
+            if (in.atEnd) Failure("end of input", in)
+            else {
+              val command = in.first
+              if (pred(command)) Success(command, in.rest)
+              else Failure("bad input", in)
+            }
+          }
+        }
+
+      def category(pred: String => Boolean, other: Boolean): Parser[Command] =
+        command(_.span.is_kind(keywords, pred, other))
+
+      def theory_element: Parser[Element[Command]] =
+        category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
+      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) }
+
+      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)
+        }
+    }
+    Parser.apply
+  }
+}
diff -r 63c9c6ceb7a3 -r 3b2daa7bf9f4 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Aug 29 18:53:29 2018 +0200
+++ b/src/Pure/build-jars	Wed Aug 29 18:53:58 2018 +0200
@@ -135,6 +135,7 @@
   Thy/latex.scala
   Thy/present.scala
   Thy/sessions.scala
+  Thy/thy_element.scala
   Thy/thy_header.scala
   Thy/thy_resources.scala
   Thy/thy_syntax.scala