# 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)
   }