# HG changeset patch
# User lcp
# Date 776681875 -7200
# Node ID 55755ed9fab927a93d6da998208168222fc139c5
# Parent  b2be4790da7a6ea29693317eda32d916b8780fe7
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
Pure/library/is_blank: now handles form feeds () too, in accordance with
ML definition

diff -r b2be4790da7a -r 55755ed9fab9 src/Pure/Syntax/pretty.ML
--- a/src/Pure/Syntax/pretty.ML	Fri Aug 12 10:20:07 1994 +0200
+++ b/src/Pure/Syntax/pretty.ML	Fri Aug 12 10:57:55 1994 +0200
@@ -37,7 +37,7 @@
   val fbreaks: T list -> T list
   val block: T list -> T
   val strs: string list -> T
-  val parents: string -> string -> T list -> T
+  val enclose: string -> string -> T list -> T
   val list: string -> string -> T list -> T
   val str_list: string -> string -> string list -> T
   val big_list: string -> T list -> T
@@ -170,11 +170,11 @@
 
 val strs = block o breaks o (map str);
 
-fun parents lpar rpar prts =
+fun enclose lpar rpar prts =
   block (str lpar :: (prts @ [str rpar]));
 
 fun list lpar rpar prts =
-  parents lpar rpar (commas prts);
+  enclose lpar rpar (commas prts);
 
 fun str_list lpar rpar strs =
   list lpar rpar (map str strs);
diff -r b2be4790da7a -r 55755ed9fab9 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Aug 12 10:20:07 1994 +0200
+++ b/src/Pure/library.ML	Fri Aug 12 10:57:55 1994 +0200
@@ -383,9 +383,9 @@
   | is_quasi_letter "'" = true
   | is_quasi_letter ch = is_letter ch;
 
-(*white space: blanks, tabs, newlines*)
+(*white space: blanks, tabs, newlines, formfeeds*)
 val is_blank : string -> bool =
-  fn " " => true | "\t" => true | "\n" => true | _ => false;
+  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | _ => false;
 
 val is_letdig = is_quasi_letter orf is_digit;
 
@@ -400,11 +400,11 @@
   in implode o (map lower) o explode end;
 
 
-(*parentesize*)
-fun parents lpar rpar str = lpar ^ str ^ rpar;
+(*enclose in brackets*)
+fun enclose lpar rpar str = lpar ^ str ^ rpar;
 
 (*simple quoting (does not escape special chars)*)
-val quote = parents "\"" "\"";
+val quote = enclose "\"" "\"";
 
 (*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
 fun space_implode a bs = implode (separate a bs);