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