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 = (0 /: body)(_ + _.length) } |
21 case class Atom(length: Int) extends Document |
21 case class Atom(length: Int) extends Document |
22 |
22 |
23 private 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) |
|
26 |
|
27 def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] = |
|
28 { |
|
29 command.span.name match { |
|
30 case Thy_Header.CHAPTER => Some(0) |
|
31 case Thy_Header.SECTION => Some(1) |
|
32 case Thy_Header.SUBSECTION => Some(2) |
|
33 case Thy_Header.SUBSUBSECTION => Some(3) |
|
34 case Thy_Header.PARAGRAPH => Some(4) |
|
35 case Thy_Header.SUBPARAGRAPH => Some(5) |
|
36 case _ if is_theory_command(keywords, command) => Some(6) |
|
37 case _ => None |
|
38 } |
|
39 } |
26 |
40 |
27 |
41 |
28 |
42 |
29 /** context blocks **/ |
43 /** context blocks **/ |
30 |
44 |
135 |
149 |
136 private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item |
150 private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item |
137 { |
151 { |
138 override def name: String = command.span.name |
152 override def name: String = command.span.name |
139 override def source: String = command.source |
153 override def source: String = command.source |
140 override def heading_level: Option[Int] = |
154 override def heading_level: Option[Int] = Document_Structure.heading_level(keywords, command) |
141 { |
|
142 name match { |
|
143 case Thy_Header.CHAPTER => Some(0) |
|
144 case Thy_Header.SECTION => Some(1) |
|
145 case Thy_Header.SUBSECTION => Some(2) |
|
146 case Thy_Header.SUBSUBSECTION => Some(3) |
|
147 case Thy_Header.PARAGRAPH => Some(4) |
|
148 case Thy_Header.SUBPARAGRAPH => Some(5) |
|
149 case _ if is_theory_command(keywords, command) => Some(6) |
|
150 case _ => None |
|
151 } |
|
152 } |
|
153 } |
155 } |
154 |
156 |
155 def parse_sections( |
157 def parse_sections( |
156 syntax: Outer_Syntax, |
158 syntax: Outer_Syntax, |
157 node_name: Document.Node.Name, |
159 node_name: Document.Node.Name, |