equal
deleted
inserted
replaced
275 |
275 |
276 /* overall document structure */ |
276 /* overall document structure */ |
277 |
277 |
278 def heading_level(command: Command): Option[Int] = |
278 def heading_level(command: Command): Option[Int] = |
279 { |
279 { |
280 keyword_kind(command.name) match { |
280 command.name match { |
281 case _ if command.name == "header" => Some(0) |
281 case "chapter" => Some(0) |
282 case Some(Keyword.THY_HEADING1) => Some(1) |
282 case "section" | "header" => Some(1) |
283 case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2) |
283 case "subsection" => Some(2) |
284 case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3) |
284 case "subsubsection" => Some(3) |
285 case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4) |
285 case _ => |
286 case Some(kind) if Keyword.theory(kind) => Some(5) |
286 keyword_kind(command.name) match { |
287 case _ => None |
287 case Some(kind) if Keyword.theory(kind) => Some(4) |
|
288 case _ => None |
|
289 } |
288 } |
290 } |
289 } |
291 } |
290 |
292 |
291 def parse_document(node_name: Document.Node.Name, text: CharSequence): |
293 def parse_document(node_name: Document.Node.Name, text: CharSequence): |
292 List[Outer_Syntax.Document] = |
294 List[Outer_Syntax.Document] = |