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