some support for breakable text and paragraphs;
tuned Symbol.scanner, which operates on symbols, not characters;
--- 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)));
--- 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 =>
--- 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";
--- 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"