# HG changeset patch # User wenzelm # Date 1470217509 -7200 # Node ID 64db21931bcbfadc84b0343d2b08dae5ac26db8e # Parent 8d20875f1290a086d65218e4480dbe84372b2576 include 'begin' and 'end' structure in text folds; diff -r 8d20875f1290 -r 64db21931bcb NEWS --- a/NEWS Tue Aug 02 22:36:53 2016 +0200 +++ b/NEWS Wed Aug 03 11:45:09 2016 +0200 @@ -82,7 +82,8 @@ * Highlighting of entity def/ref positions wrt. cursor. * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' -are treated as delimiters for fold structure. +are treated as delimiters for fold structure; 'begin' and 'end' +structure of theory specifications is treated as well. * Syntactic indentation according to Isabelle outer syntax. Action "indent-lines" (shortcut C+i) indents the current line according to diff -r 8d20875f1290 -r 64db21931bcb src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Tue Aug 02 22:36:53 2016 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Wed Aug 03 11:45:09 2016 +0200 @@ -56,7 +56,8 @@ command: Boolean = false, depth: Int = 0, span_depth: Int = 0, - after_span_depth: Int = 0) + after_span_depth: Int = 0, + element_depth: Int = 0) /* overall document structure */ @@ -157,13 +158,13 @@ /* line-oriented structure */ private val close_structure = - Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE) + Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END) def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure) : Outer_Syntax.Line_Structure = { val improper1 = tokens.forall(_.is_improper) - val command1 = tokens.exists(_.is_command) + val command1 = tokens.exists(_.is_begin_or_command) val command_depth = tokens.iterator.filter(_.is_proper).toStream.headOption match { @@ -174,31 +175,36 @@ case None => None } + val depth0 = structure.element_depth val depth1 = if (tokens.exists(tok => - keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory))) 0 + keywords.is_before_command(tok) || + !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0 else if (command_depth.isDefined) command_depth.get else if (command1) structure.after_span_depth else structure.span_depth - val (span_depth1, after_span_depth1) = - ((structure.span_depth, structure.after_span_depth) /: tokens) { - case ((x, y), tok) => - if (tok.is_command) { - if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1) - else if (keywords.is_command(tok, Keyword.theory)) (1, 0) - else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1) - else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1) - else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2) - else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1) - else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1) - else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0) - else (x, y) + val (span_depth1, after_span_depth1, element_depth1) = + ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) { + case (depths @ (x, y, z), tok) => + if (tok.is_begin) (z + 2, z + 1, z + 1) + else if (tok.is_end) (z + 1, z - 1, z - 1) + else if (tok.is_command) { + if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z) + else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z) + else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z) + else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z) + else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z) + else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z) + else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z) + else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z) + else depths } - else (x, y) + else depths } - Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1) + Outer_Syntax.Line_Structure( + improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1) }