# HG changeset patch
# User wenzelm
# Date 1355572511 -3600
# Node ID 00bdc48c5f71a1a5ac94cdf80663d11b811b577e
# Parent  c76b41cde4f57e0db954870911169381188b2248
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;

diff -r c76b41cde4f5 -r 00bdc48c5f71 src/Pure/General/pretty.ML
--- 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];
 
diff -r c76b41cde4f5 -r 00bdc48c5f71 src/Pure/PIDE/markup.ML
--- 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 *)
diff -r c76b41cde4f5 -r 00bdc48c5f71 src/Pure/PIDE/markup.scala
--- 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 */
diff -r c76b41cde4f5 -r 00bdc48c5f71 src/Tools/jEdit/src/rendering.scala
--- 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), _ =>