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