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