--- a/src/Pure/General/pretty.ML Sat Dec 15 12:54:14 2012 +0100
+++ b/src/Pure/General/pretty.ML Sat Dec 15 12:55:11 2012 +0100
@@ -163,9 +163,11 @@
val paragraph = markup Markup.paragraph;
val para = paragraph o text;
-fun markup_chunks m prts = markup m (fbreaks prts);
+fun markup_chunks m prts = markup m (fbreaks (map (mark Markup.text_fold) prts));
val chunks = markup_chunks Markup.empty;
-fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
+
+fun chunks2 prts =
+ blk (0, flat (Library.separate [fbrk, fbrk] (map (single o mark Markup.text_fold) prts)));
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
--- a/src/Pure/PIDE/markup.ML Sat Dec 15 12:54:14 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Dec 15 12:55:11 2012 +0100
@@ -77,6 +77,7 @@
val document_antiquotationN: string
val document_antiquotation_optionN: string
val paragraphN: string val paragraph: T
+ val text_foldN: string val text_fold: T
val keywordN: string val keyword: T
val operatorN: string val operator: T
val commandN: string val command: T
@@ -298,6 +299,7 @@
(* text structure *)
val (paragraphN, paragraph) = markup_elem "paragraph";
+val (text_foldN, text_fold) = markup_elem "text_fold";
(* outer syntax *)
--- a/src/Pure/PIDE/markup.scala Sat Dec 15 12:54:14 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Dec 15 12:55:11 2012 +0100
@@ -145,6 +145,7 @@
/* text structure */
val PARAGRAPH = "paragraph"
+ val TEXT_FOLD = "text_fold"
/* ML syntax */
--- a/src/Tools/jEdit/src/rendering.scala Sat Dec 15 12:54:14 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Dec 15 12:55:11 2012 +0100
@@ -531,7 +531,7 @@
/* nested text structure -- folds */
- private val fold_depth_include = Set(Markup.GOAL, Markup.SUBGOAL)
+ private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>