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;
     1 /*  Title:      Pure/Isar/line_structure.scala
     2     Author:     Makarius
     3 
     4 Line-oriented document structure, e.g. for fold handling.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Line_Structure
    11 {
    12   val init = Line_Structure()
    13 }
    14 
    15 sealed 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 }