explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
authorwenzelm
Sat Dec 15 12:55:11 2012 +0100 (2012-12-15 ago)
changeset 5054500bdc48c5f71
parent 50544 c76b41cde4f5
child 50546 1b01a57d2749
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
src/Pure/General/pretty.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/pretty.ML	Sat Dec 15 12:54:14 2012 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Dec 15 12:55:11 2012 +0100
     1.3 @@ -163,9 +163,11 @@
     1.4  val paragraph = markup Markup.paragraph;
     1.5  val para = paragraph o text;
     1.6  
     1.7 -fun markup_chunks m prts = markup m (fbreaks prts);
     1.8 +fun markup_chunks m prts = markup m (fbreaks (map (mark Markup.text_fold) prts));
     1.9  val chunks = markup_chunks Markup.empty;
    1.10 -fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
    1.11 +
    1.12 +fun chunks2 prts =
    1.13 +  blk (0, flat (Library.separate [fbrk, fbrk] (map (single o mark Markup.text_fold) prts)));
    1.14  
    1.15  fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
    1.16  
     2.1 --- a/src/Pure/PIDE/markup.ML	Sat Dec 15 12:54:14 2012 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Sat Dec 15 12:55:11 2012 +0100
     2.3 @@ -77,6 +77,7 @@
     2.4    val document_antiquotationN: string
     2.5    val document_antiquotation_optionN: string
     2.6    val paragraphN: string val paragraph: T
     2.7 +  val text_foldN: string val text_fold: T
     2.8    val keywordN: string val keyword: T
     2.9    val operatorN: string val operator: T
    2.10    val commandN: string val command: T
    2.11 @@ -298,6 +299,7 @@
    2.12  (* text structure *)
    2.13  
    2.14  val (paragraphN, paragraph) = markup_elem "paragraph";
    2.15 +val (text_foldN, text_fold) = markup_elem "text_fold";
    2.16  
    2.17  
    2.18  (* outer syntax *)
     3.1 --- a/src/Pure/PIDE/markup.scala	Sat Dec 15 12:54:14 2012 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Sat Dec 15 12:55:11 2012 +0100
     3.3 @@ -145,6 +145,7 @@
     3.4    /* text structure */
     3.5  
     3.6    val PARAGRAPH = "paragraph"
     3.7 +  val TEXT_FOLD = "text_fold"
     3.8  
     3.9  
    3.10    /* ML syntax */
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:54:14 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:55:11 2012 +0100
     4.3 @@ -531,7 +531,7 @@
     4.4  
     4.5    /* nested text structure -- folds */
     4.6  
     4.7 -  private val fold_depth_include = Set(Markup.GOAL, Markup.SUBGOAL)
     4.8 +  private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
     4.9  
    4.10    def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
    4.11      snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>