1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Dec 15 12:01:07 2012 +0100
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Dec 15 12:16:16 2012 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    "src/dockable.scala"
     1.5    "src/document_model.scala"
     1.6    "src/document_view.scala"
     1.7 +  "src/fold_handling.scala"
     1.8    "src/graphview_dockable.scala"
     1.9    "src/html_panel.scala"
    1.10    "src/hyperlink.scala"

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Sat Dec 15 12:16:16 2012 +0100
     2.3 @@ -0,0 +1,48 @@
     2.4 +/*  Title:      Tools/jEdit/src/fold_handler.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Handling of folds within the text structure.
     2.8 +*/
     2.9 +
    2.10 +package isabelle.jedit
    2.11 +
    2.12 +
    2.13 +import isabelle._
    2.14 +
    2.15 +import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
    2.16 +
    2.17 +import javax.swing.text.Segment
    2.18 +
    2.19 +
    2.20 +object Fold_Handling
    2.21 +{
    2.22 +  class Document_Fold_Handler(private val rendering: Rendering)
    2.23 +    extends FoldHandler("isabelle-document")
    2.24 +  {
    2.25 +    override def equals(other: Any): Boolean =
    2.26 +      other match {
    2.27 +        case that: Document_Fold_Handler => this.rendering == that.rendering
    2.28 +        case _ => false
    2.29 +      }
    2.30 +
    2.31 +    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
    2.32 +    {
    2.33 +      def depth(i: Text.Offset): Int =
    2.34 +        if (i < 0) 0
    2.35 +        else {
    2.36 +          rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
    2.37 +            case d #:: _ => d
    2.38 +            case _ => 0
    2.39 +          }
    2.40 +        }
    2.41 +
    2.42 +      if (line <= 0) 0
    2.43 +      else {
    2.44 +        val start = buffer.getLineStartOffset(line - 1)
    2.45 +        val end = buffer.getLineEndOffset(line - 1)
    2.46 +        buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1)
    2.47 +      }
    2.48 +    }
    2.49 +  }
    2.50 +}
    2.51 +

     3.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Dec 15 12:01:07 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Dec 15 12:16:16 2012 +0100
     3.3 @@ -16,6 +16,7 @@
     3.4  
     3.5  import org.gjt.sp.jedit.{jEdit, View, Registers}
     3.6  import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
     3.7 +import org.gjt.sp.jedit.syntax.SyntaxStyle
     3.8  import org.gjt.sp.util.SyntaxUtilities
     3.9  
    3.10  
    3.11 @@ -82,6 +83,15 @@
    3.12      getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    3.13      getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
    3.14  
    3.15 +    val fold_line_style = new Array[SyntaxStyle](4)
    3.16 +    for (i <- 0 to 3) {
    3.17 +      fold_line_style(i) =
    3.18 +        SyntaxUtilities.parseStyle(
    3.19 +          jEdit.getProperty("view.style.foldLine." + i),
    3.20 +          current_font_family, current_font_size, true)
    3.21 +    }
    3.22 +    getPainter.setFoldLineStyle(fold_line_style)
    3.23 +
    3.24      if (getWidth > 0) {
    3.25        getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
    3.26        getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
    3.27 @@ -117,6 +127,7 @@
    3.28              JEdit_Lib.buffer_edit(getBuffer) {
    3.29                rich_text_area.active_reset()
    3.30                getBuffer.setReadOnly(false)
    3.31 +              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
    3.32                setText(text)
    3.33                setCaretPosition(0)
    3.34                getBuffer.setReadOnly(true)

     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:01:07 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:16:16 2012 +0100
     4.3 @@ -527,4 +527,16 @@
     4.4            if text_colors.isDefinedAt(m) => text_colors(m)
     4.5          })
     4.6    }
     4.7 +
     4.8 +
     4.9 +  /* nested text structure -- folds */
    4.10 +
    4.11 +  private val fold_depth_include = Set(Markup.SUBGOAL)
    4.12 +
    4.13 +  def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
    4.14 +    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
    4.15 +      {
    4.16 +        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
    4.17 +        if fold_depth_include(name) => depth + 1
    4.18 +      })
    4.19  }