# HG changeset patch
# User wenzelm
# Date 1355570176 -3600
# Node ID 58bd88159f8f2ac9d15b29302de3642efb9876be
# Parent  021f054ff1faedb0922d7c59084c06e9fb00a90c
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
fold subgoals;

diff -r 021f054ff1fa -r 58bd88159f8f src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Dec 15 12:01:07 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Dec 15 12:16:16 2012 +0100
@@ -12,6 +12,7 @@
   "src/dockable.scala"
   "src/document_model.scala"
   "src/document_view.scala"
+  "src/fold_handling.scala"
   "src/graphview_dockable.scala"
   "src/html_panel.scala"
   "src/hyperlink.scala"
diff -r 021f054ff1fa -r 58bd88159f8f src/Tools/jEdit/src/fold_handling.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/fold_handling.scala	Sat Dec 15 12:16:16 2012 +0100
@@ -0,0 +1,48 @@
+/*  Title:      Tools/jEdit/src/fold_handler.scala
+    Author:     Makarius
+
+Handling of folds within the text structure.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
+
+import javax.swing.text.Segment
+
+
+object Fold_Handling
+{
+  class Document_Fold_Handler(private val rendering: Rendering)
+    extends FoldHandler("isabelle-document")
+  {
+    override def equals(other: Any): Boolean =
+      other match {
+        case that: Document_Fold_Handler => this.rendering == that.rendering
+        case _ => false
+      }
+
+    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
+    {
+      def depth(i: Text.Offset): Int =
+        if (i < 0) 0
+        else {
+          rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
+            case d #:: _ => d
+            case _ => 0
+          }
+        }
+
+      if (line <= 0) 0
+      else {
+        val start = buffer.getLineStartOffset(line - 1)
+        val end = buffer.getLineEndOffset(line - 1)
+        buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1)
+      }
+    }
+  }
+}
+
diff -r 021f054ff1fa -r 58bd88159f8f src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Dec 15 12:01:07 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Dec 15 12:16:16 2012 +0100
@@ -16,6 +16,7 @@
 
 import org.gjt.sp.jedit.{jEdit, View, Registers}
 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
+import org.gjt.sp.jedit.syntax.SyntaxStyle
 import org.gjt.sp.util.SyntaxUtilities
 
 
@@ -82,6 +83,15 @@
     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
     getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
 
+    val fold_line_style = new Array[SyntaxStyle](4)
+    for (i <- 0 to 3) {
+      fold_line_style(i) =
+        SyntaxUtilities.parseStyle(
+          jEdit.getProperty("view.style.foldLine." + i),
+          current_font_family, current_font_size, true)
+    }
+    getPainter.setFoldLineStyle(fold_line_style)
+
     if (getWidth > 0) {
       getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
       getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
@@ -117,6 +127,7 @@
             JEdit_Lib.buffer_edit(getBuffer) {
               rich_text_area.active_reset()
               getBuffer.setReadOnly(false)
+              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
               setText(text)
               setCaretPosition(0)
               getBuffer.setReadOnly(true)
diff -r 021f054ff1fa -r 58bd88159f8f src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:01:07 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:16:16 2012 +0100
@@ -527,4 +527,16 @@
           if text_colors.isDefinedAt(m) => text_colors(m)
         })
   }
+
+
+  /* nested text structure -- folds */
+
+  private val fold_depth_include = Set(Markup.SUBGOAL)
+
+  def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
+    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
+      {
+        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
+        if fold_depth_include(name) => depth + 1
+      })
 }