1/*  Title:      Pure/Isar/line_structure.scala
2    Author:     Makarius
3
4Line-oriented document structure, e.g. for fold handling.
5*/
6
7package isabelle
8
9
10object Line_Structure
11{
12  val init = Line_Structure()
13}
14
15sealed case class Line_Structure(
16  improper: Boolean = true,
17  blank: Boolean = true,
18  command: Boolean = false,
19  depth: Int = 0,
20  span_depth: Int = 0,
21  after_span_depth: Int = 0,
22  element_depth: Int = 0)
23{
24  def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
25  {
26    val improper1 = tokens.forall(tok => !tok.is_proper)
27    val blank1 = tokens.forall(_.is_space)
28    val command1 = tokens.exists(_.is_begin_or_command)
29
30    val command_depth =
31      tokens.iterator.filter(_.is_proper).toStream.headOption match {
32        case Some(tok) =>
33          if (keywords.is_command(tok, Keyword.close_structure))
34            Some(after_span_depth - 1)
35          else None
36        case None => None
37      }
38
39    val depth1 =
40      if (tokens.exists(tok =>
41            keywords.is_before_command(tok) ||
42            !tok.is_end && keywords.is_command(tok, Keyword.theory))) element_depth
43      else if (command_depth.isDefined) command_depth.get
44      else if (command1) after_span_depth
45      else span_depth
46
47    val (span_depth1, after_span_depth1, element_depth1) =
48      ((span_depth, after_span_depth, element_depth) /: tokens) {
49        case (depths @ (x, y, z), tok) =>
50          if (tok.is_begin) (z + 2, z + 1, z + 1)
51          else if (tok.is_end) (z + 1, z - 1, z - 1)
52          else if (tok.is_command) {
53            val depth0 = element_depth
54            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
55            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
56            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
57            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
58            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
59            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
60            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
61            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
62            else depths
63          }
64          else depths
65      }
66
67    Line_Structure(
68      improper1, blank1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
69  }
70}
71