1/* Title: Pure/Isar/document_structure.scala 2 Author: Makarius 3 4Overall document structure. 5*/ 6 7package isabelle 8 9 10import scala.collection.mutable 11import scala.annotation.tailrec 12 13 14object Document_Structure 15{ 16 /** general structure **/ 17 18 sealed abstract class Document { def length: Int } 19 case class Block(name: String, text: String, body: List[Document]) extends Document 20 { val length: Int = (0 /: body)(_ + _.length) } 21 case class Atom(length: Int) extends Document 22 23 private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean = 24 keywords.kinds.get(name) match { 25 case Some(kind) => Keyword.theory(kind) && !Keyword.theory_end(kind) 26 case None => false 27 } 28 29 30 31 /** context blocks **/ 32 33 def parse_blocks( 34 syntax: Outer_Syntax, 35 node_name: Document.Node.Name, 36 text: CharSequence): List[Document] = 37 { 38 def is_plain_theory(command: Command): Boolean = 39 is_theory_command(syntax.keywords, command.span.name) && 40 !command.span.is_begin && !command.span.is_end 41 42 43 /* stack operations */ 44 45 def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document] 46 47 var stack: List[(Command, mutable.ListBuffer[Document])] = 48 List((Command.empty, buffer())) 49 50 def open(command: Command) { stack = (command, buffer()) :: stack } 51 52 def close(): Boolean = 53 stack match { 54 case (command, body) :: (_, body2) :: _ => 55 body2 += Block(command.span.name, command.source, body.toList) 56 stack = stack.tail 57 true 58 case _ => 59 false 60 } 61 62 def flush() { if (is_plain_theory(stack.head._1)) close() } 63 64 def result(): List[Document] = 65 { 66 while (close()) { } 67 stack.head._2.toList 68 } 69 70 def add(command: Command) 71 { 72 if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) } 73 else if (command.span.is_end) { flush(); close() } 74 75 stack.head._2 += Atom(command.source.length) 76 } 77 78 79 /* result structure */ 80 81 val spans = syntax.parse_spans(text) 82 spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span))) 83 result() 84 } 85 86 87 88 /** section headings **/ 89 90 trait Item 91 { 92 def name: String = "" 93 def source: String = "" 94 def heading_level: Option[Int] = None 95 } 96 97 object No_Item extends Item 98 99 class Sections(keywords: Keyword.Keywords) 100 { 101 private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document] 102 103 private var stack: List[(Int, Item, mutable.ListBuffer[Document])] = 104 List((0, No_Item, buffer())) 105 106 @tailrec private def close(level: Int => Boolean) 107 { 108 stack match { 109 case (lev, item, body) :: (_, _, body2) :: _ if level(lev) => 110 body2 += Block(item.name, item.source, body.toList) 111 stack = stack.tail 112 close(level) 113 case _ => 114 } 115 } 116 117 def result(): List[Document] = 118 { 119 close(_ => true) 120 stack.head._3.toList 121 } 122 123 def add(item: Item) 124 { 125 item.heading_level match { 126 case Some(i) => 127 close(_ > i) 128 stack = (i + 1, item, buffer()) :: stack 129 case None => 130 } 131 stack.head._3 += Atom(item.source.length) 132 } 133 } 134 135 136 /* outer syntax sections */ 137 138 private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item 139 { 140 override def name: String = command.span.name 141 override def source: String = command.source 142 override def heading_level: Option[Int] = 143 { 144 name match { 145 case Thy_Header.CHAPTER => Some(0) 146 case Thy_Header.SECTION => Some(1) 147 case Thy_Header.SUBSECTION => Some(2) 148 case Thy_Header.SUBSUBSECTION => Some(3) 149 case Thy_Header.PARAGRAPH => Some(4) 150 case Thy_Header.SUBPARAGRAPH => Some(5) 151 case _ if is_theory_command(keywords, name) => Some(6) 152 case _ => None 153 } 154 } 155 } 156 157 def parse_sections( 158 syntax: Outer_Syntax, 159 node_name: Document.Node.Name, 160 text: CharSequence): List[Document] = 161 { 162 val sections = new Sections(syntax.keywords) 163 164 for { span <- syntax.parse_spans(text) } { 165 sections.add( 166 new Command_Item(syntax.keywords, 167 Command(Document_ID.none, node_name, Command.no_blobs, span))) 168 } 169 sections.result() 170 } 171 172 173 /* ML sections */ 174 175 private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item 176 { 177 override def source: String = token.source 178 override def heading_level: Option[Int] = level 179 } 180 181 def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] = 182 { 183 val sections = new Sections(Keyword.Keywords.empty) 184 val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None) 185 186 var context: Scan.Line_Context = Scan.Finished 187 for (line <- Library.separated_chunks(_ == '\n', text)) { 188 val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context) 189 val level = 190 toks.filterNot(_.is_space) match { 191 case List(tok) if tok.is_comment => 192 val s = tok.source 193 if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c))) 194 { 195 if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0) 196 else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1) 197 else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2) 198 else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3) 199 else None 200 } 201 else None 202 case _ => None 203 } 204 if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished) 205 toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None))) 206 else 207 toks.foreach(tok => sections.add(new ML_Item(tok, None))) 208 209 sections.add(nl) 210 context = next_context 211 } 212 sections.result() 213 } 214} 215