# HG changeset patch
# User wenzelm
# Date 1413658576 -7200
# Node ID 4717d18cc6191c2f399bd0ae84fe4b2beecc6651
# Parent  e46afcceb78159c1054ddb84eaba0b3529458de9
clarified Line_Structure wrt. command span;

diff -r e46afcceb781 -r 4717d18cc619 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 11:19:34 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 20:56:16 2014 +0200
@@ -43,10 +43,15 @@
 
   object Line_Structure
   {
-    val init = Line_Structure(0, 0)
+    val init = Line_Structure()
   }
 
-  sealed case class Line_Structure(depth_before: Int, depth: Int)
+  sealed case class Line_Structure(
+    improper: Boolean = true,
+    command: Boolean = false,
+    depth: Int = 0,
+    span_depth: Int = 0,
+    after_span_depth: Int = 0)
 }
 
 final class Outer_Syntax private(
@@ -150,21 +155,29 @@
 
   /* line-oriented structure */
 
-  def line_structure(tokens: List[Token], depth: Int): Outer_Syntax.Line_Structure =
+  def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
+    : Outer_Syntax.Line_Structure =
   {
+    val improper1 = tokens.forall(_.is_improper)
+    val command1 = tokens.exists(_.is_command)
+
     val depth1 =
       if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
-      else depth
-    val depth2 =
-      (depth /: tokens) { case (d, tok) =>
-        if (command_kind(tok, Keyword.theory_goal)) 1
-        else if (command_kind(tok, Keyword.theory)) 0
-        else if (command_kind(tok, Keyword.proof_goal)) d + 1
-        else if (command_kind(tok, Keyword.qed)) d - 1
-        else if (command_kind(tok, Keyword.qed_global)) 0
-        else d
+      else if (command1) struct.after_span_depth
+      else struct.span_depth
+
+    val (span_depth1, after_span_depth1) =
+      ((struct.span_depth, struct.after_span_depth) /: tokens) {
+        case ((d0, d), tok) =>
+          if (command_kind(tok, Keyword.theory_goal)) (2, 1)
+          else if (command_kind(tok, Keyword.theory)) (1, 0)
+          else if (command_kind(tok, Keyword.proof_goal)) (d + 2, d + 1)
+          else if (command_kind(tok, Keyword.qed)) (d + 1, d - 1)
+          else if (command_kind(tok, Keyword.qed_global)) (1, 0)
+          else (d0, d)
       }
-    Outer_Syntax.Line_Structure(depth1, depth2)
+
+    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
   }
 
 
@@ -197,7 +210,7 @@
       }
     }
     val tokens = toks.toList
-    (tokens, ctxt, line_structure(tokens, structure.depth))
+    (tokens, ctxt, line_structure(tokens, structure))
   }
 
 
diff -r e46afcceb781 -r 4717d18cc619 src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala	Sat Oct 18 11:19:34 2014 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Sat Oct 18 20:56:16 2014 +0200
@@ -9,9 +9,11 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
+import javax.swing.text.Segment
 
-import javax.swing.text.Segment
+import scala.collection.convert.WrapAsJava
+
+import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
 
 
 object Fold_Handling
@@ -27,7 +29,22 @@
       }
 
     override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
-      Token_Markup.buffer_line_structure(buffer, line).depth_before
+      Token_Markup.buffer_line_structure(buffer, line).depth max 0
+
+    override def getPrecedingFoldLevels(
+      buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
+    {
+      val struct = Token_Markup.buffer_line_structure(buffer, line)
+      val result =
+        if (line > 0 && struct.command)
+          Range.inclusive(line - 1, 0, -1).iterator.
+            map(Token_Markup.buffer_line_structure(buffer, _)).
+            takeWhile(_.improper).map(_ => struct.depth max 0).toList
+        else Nil
+
+      if (result.isEmpty) null
+      else WrapAsJava.seqAsJavaList(result.map(i => new Integer(i)))
+    }
   }