equal
deleted
inserted
replaced
15 { |
15 { |
16 /** general structure **/ |
16 /** general structure **/ |
17 |
17 |
18 sealed abstract class Document { def length: Int } |
18 sealed abstract class Document { def length: Int } |
19 case class Block(name: String, text: String, body: List[Document]) extends Document |
19 case class Block(name: String, text: String, body: List[Document]) extends Document |
20 { val length: Int = (0 /: body)(_ + _.length) } |
20 { val length: Int = body.foldLeft(0)(_ + _.length) } |
21 case class Atom(length: Int) extends Document |
21 case class Atom(length: Int) extends Document |
22 |
22 |
23 def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean = |
23 def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean = |
24 command.span.is_kind(keywords, |
24 command.span.is_kind(keywords, |
25 kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false) |
25 kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false) |