support Thy_Element in Scala, following ML version;
authorwenzelm
Wed Aug 29 18:53:58 2018 +0200 (22 months ago)
changeset 688453b2daa7bf9f4
parent 68844 63c9c6ceb7a3
child 68846 da0cb00a4d6a
support Thy_Element in Scala, following ML version;
src/Pure/Isar/document_structure.scala
src/Pure/PIDE/command_span.scala
src/Pure/Thy/thy_element.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Isar/document_structure.scala	Wed Aug 29 18:53:29 2018 +0200
     1.2 +++ b/src/Pure/Isar/document_structure.scala	Wed Aug 29 18:53:58 2018 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4    case class Atom(length: Int) extends Document
     1.5  
     1.6    private def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
     1.7 -    command.span.is_kind(keywords, kind => Keyword.theory(kind) && !Keyword.theory_end(kind))
     1.8 +    command.span.is_kind(keywords,
     1.9 +      kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
    1.10  
    1.11  
    1.12  
     2.1 --- a/src/Pure/PIDE/command_span.scala	Wed Aug 29 18:53:29 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command_span.scala	Wed Aug 29 18:53:58 2018 +0200
     2.3 @@ -39,10 +39,10 @@
     2.4          case _ => start
     2.5        }
     2.6  
     2.7 -    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
     2.8 +    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean =
     2.9        keywords.kinds.get(name) match {
    2.10          case Some(k) => pred(k)
    2.11 -        case None => false
    2.12 +        case None => other
    2.13        }
    2.14  
    2.15      def is_begin: Boolean = content.exists(_.is_begin)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Thy/thy_element.scala	Wed Aug 29 18:53:58 2018 +0200
     3.3 @@ -0,0 +1,88 @@
     3.4 +/*  Title:      Pure/Thy/thy_element.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Theory elements: statements with optional proof.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +import scala.util.parsing.combinator.Parsers
    3.13 +import scala.util.parsing.input
    3.14 +
    3.15 +
    3.16 +object Thy_Element
    3.17 +{
    3.18 +  /* datatype element */
    3.19 +
    3.20 +  type Proof[A] = (List[Element[A]], A)
    3.21 +  sealed case class Element[A](head: A, proof: Option[Proof[A]])
    3.22 +  {
    3.23 +    def iterator: Iterator[A] =
    3.24 +      Iterator(head) ++
    3.25 +        (for {
    3.26 +          (prf, qed) <- proof.iterator
    3.27 +          b <- (for (elem <- prf.iterator; a <- elem.iterator) yield a) ++ Iterator(qed)
    3.28 +        } yield b)
    3.29 +
    3.30 +    def last: A =
    3.31 +      proof match {
    3.32 +        case None => head
    3.33 +        case Some((_, qed)) => qed
    3.34 +      }
    3.35 +  }
    3.36 +
    3.37 +  def element[A](a: A, b: Proof[A]): Element[A] = Element(a, Some(b))
    3.38 +  def atom[A](a: A): Element[A] = Element(a, None)
    3.39 +
    3.40 +
    3.41 +  /* parse elements */
    3.42 +
    3.43 +  def parse_elements(keywords: Keyword.Keywords, commands: List[Command]): List[Element[Command]] =
    3.44 +  {
    3.45 +    case class Reader(in: List[Command]) extends input.Reader[Command]
    3.46 +    {
    3.47 +      def first: Command = in.head
    3.48 +      def rest: Reader = Reader(in.tail)
    3.49 +      def pos: input.Position = input.NoPosition
    3.50 +      def atEnd: Boolean = in.isEmpty
    3.51 +    }
    3.52 +
    3.53 +    object Parser extends Parsers
    3.54 +    {
    3.55 +      type Elem = Command
    3.56 +
    3.57 +      def command(pred: Command => Boolean): Parser[Command] =
    3.58 +        new Parser[Elem] {
    3.59 +          def apply(in: Input) =
    3.60 +          {
    3.61 +            if (in.atEnd) Failure("end of input", in)
    3.62 +            else {
    3.63 +              val command = in.first
    3.64 +              if (pred(command)) Success(command, in.rest)
    3.65 +              else Failure("bad input", in)
    3.66 +            }
    3.67 +          }
    3.68 +        }
    3.69 +
    3.70 +      def category(pred: String => Boolean, other: Boolean): Parser[Command] =
    3.71 +        command(_.span.is_kind(keywords, pred, other))
    3.72 +
    3.73 +      def theory_element: Parser[Element[Command]] =
    3.74 +        category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) }
    3.75 +      def proof_element: Parser[Element[Command]] =
    3.76 +        category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } |
    3.77 +        category(Keyword.proof_body, true) ^^ { case a => atom(a) }
    3.78 +      def proof: Parser[Proof[Command]] =
    3.79 +        rep(proof_element) ~ category(Keyword.qed, false) ^^ { case a ~ b => (a, b) }
    3.80 +
    3.81 +      val default_element: Parser[Element[Command]] = command(_ => true) ^^ { case a => atom(a) }
    3.82 +
    3.83 +      def apply: List[Element[Command]] =
    3.84 +        rep(theory_element | default_element)(Reader(commands)) match {
    3.85 +          case Success(result, rest) if rest.atEnd => result
    3.86 +          case bad => error(bad.toString)
    3.87 +        }
    3.88 +    }
    3.89 +    Parser.apply
    3.90 +  }
    3.91 +}
     4.1 --- a/src/Pure/build-jars	Wed Aug 29 18:53:29 2018 +0200
     4.2 +++ b/src/Pure/build-jars	Wed Aug 29 18:53:58 2018 +0200
     4.3 @@ -135,6 +135,7 @@
     4.4    Thy/latex.scala
     4.5    Thy/present.scala
     4.6    Thy/sessions.scala
     4.7 +  Thy/thy_element.scala
     4.8    Thy/thy_header.scala
     4.9    Thy/thy_resources.scala
    4.10    Thy/thy_syntax.scala