# HG changeset patch
# User wenzelm
# Date 1353583323 -3600
# Node ID e06eabc421e7ee248bb138836b3e309c1af38fb3
# Parent  4fc4237488abaddd65ca7f760651631140663917
some support for breakable text and paragraphs;
tuned Symbol.scanner, which operates on symbols, not characters;

diff -r 4fc4237488ab -r e06eabc421e7 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Nov 22 08:23:13 2012 +0100
+++ b/src/Pure/General/pretty.ML	Thu Nov 22 12:22:03 2012 +0100
@@ -40,6 +40,9 @@
   val marks_str: Markup.T list * string -> T
   val command: string -> T
   val keyword: string -> T
+  val text: string -> T list
+  val paragraph: T list -> T
+  val para: string -> T
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
@@ -156,6 +159,10 @@
 fun command name = mark_str (Isabelle_Markup.keyword1, name);
 fun keyword name = mark_str (Isabelle_Markup.keyword2, name);
 
+val text = breaks o map str o Symbol.explode_words;
+val paragraph = markup Isabelle_Markup.paragraph;
+val para = paragraph o text;
+
 fun markup_chunks m prts = markup m (fbreaks prts);
 val chunks = markup_chunks Markup.empty;
 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
diff -r 4fc4237488ab -r e06eabc421e7 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Nov 22 08:23:13 2012 +0100
+++ b/src/Pure/General/symbol.ML	Thu Nov 22 12:22:03 2012 +0100
@@ -56,6 +56,8 @@
   val scan_id: string list -> string * string list
   val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
+  val split_words: symbol list -> string list
+  val explode_words: string -> string list
   val esc: symbol -> string
   val escape: string -> string
   val strip_blanks: string -> string
@@ -170,7 +172,7 @@
         val raw0 = enclose "\\<^raw:" ">";
         val raw1 = raw0 o implode;
         val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
-    
+
         fun encode cs = enc (take_prefix raw_chr cs)
         and enc ([], []) = []
           | enc (cs, []) = [raw1 cs]
@@ -399,13 +401,13 @@
 
 (* scanning through symbols *)
 
-fun scanner msg scan chs =
+fun scanner msg scan syms =
   let
-    fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs))
-      | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs));
-    val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
+    fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
+      | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss));
+    val finite_scan = Scan.error (Scan.finite stopper (!! message scan));
   in
-    (case fin_scan chs of
+    (case finite_scan syms of
       (result, []) => result
     | (_, rest) => error (message (rest, NONE) ()))
   end;
@@ -470,6 +472,17 @@
 end;
 
 
+(* space-separated words *)
+
+val scan_word =
+  Scan.many1 is_ascii_blank >> K NONE ||
+  Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);
+
+val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
+
+val explode_words = split_words o sym_explode;
+
+
 (* escape *)
 
 val esc = fn s =>
diff -r 4fc4237488ab -r e06eabc421e7 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Nov 22 08:23:13 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Nov 22 12:22:03 2012 +0100
@@ -67,6 +67,7 @@
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
+  val paragraphN: string val paragraph: Markup.T
   val keywordN: string val keyword: Markup.T
   val operatorN: string val operator: Markup.T
   val commandN: string val command: Markup.T
@@ -239,6 +240,11 @@
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
+(* text structure *)
+
+val (paragraphN, paragraph) = markup_elem "paragraph";
+
+
 (* outer syntax *)
 
 val (keywordN, keyword) = markup_elem "keyword";
diff -r 4fc4237488ab -r e06eabc421e7 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Nov 22 08:23:13 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Nov 22 12:22:03 2012 +0100
@@ -126,6 +126,11 @@
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
+  /* text structure */
+
+  val PARAGRAPH = "paragraph"
+
+
   /* ML syntax */
 
   val ML_KEYWORD = "ML_keyword"