Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
authorlcp
Fri Aug 12 10:57:55 1994 +0200 (1994-08-12)
changeset 51255755ed9fab9
parent 511 b2be4790da7a
child 513 97a879e8d01b
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
Pure/library/is_blank: now handles form feeds () too, in accordance with
ML definition
src/Pure/Syntax/pretty.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Syntax/pretty.ML	Fri Aug 12 10:20:07 1994 +0200
     1.2 +++ b/src/Pure/Syntax/pretty.ML	Fri Aug 12 10:57:55 1994 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    val fbreaks: T list -> T list
     1.5    val block: T list -> T
     1.6    val strs: string list -> T
     1.7 -  val parents: string -> string -> T list -> T
     1.8 +  val enclose: string -> string -> T list -> T
     1.9    val list: string -> string -> T list -> T
    1.10    val str_list: string -> string -> string list -> T
    1.11    val big_list: string -> T list -> T
    1.12 @@ -170,11 +170,11 @@
    1.13  
    1.14  val strs = block o breaks o (map str);
    1.15  
    1.16 -fun parents lpar rpar prts =
    1.17 +fun enclose lpar rpar prts =
    1.18    block (str lpar :: (prts @ [str rpar]));
    1.19  
    1.20  fun list lpar rpar prts =
    1.21 -  parents lpar rpar (commas prts);
    1.22 +  enclose lpar rpar (commas prts);
    1.23  
    1.24  fun str_list lpar rpar strs =
    1.25    list lpar rpar (map str strs);
     2.1 --- a/src/Pure/library.ML	Fri Aug 12 10:20:07 1994 +0200
     2.2 +++ b/src/Pure/library.ML	Fri Aug 12 10:57:55 1994 +0200
     2.3 @@ -383,9 +383,9 @@
     2.4    | is_quasi_letter "'" = true
     2.5    | is_quasi_letter ch = is_letter ch;
     2.6  
     2.7 -(*white space: blanks, tabs, newlines*)
     2.8 +(*white space: blanks, tabs, newlines, formfeeds*)
     2.9  val is_blank : string -> bool =
    2.10 -  fn " " => true | "\t" => true | "\n" => true | _ => false;
    2.11 +  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | _ => false;
    2.12  
    2.13  val is_letdig = is_quasi_letter orf is_digit;
    2.14  
    2.15 @@ -400,11 +400,11 @@
    2.16    in implode o (map lower) o explode end;
    2.17  
    2.18  
    2.19 -(*parentesize*)
    2.20 -fun parents lpar rpar str = lpar ^ str ^ rpar;
    2.21 +(*enclose in brackets*)
    2.22 +fun enclose lpar rpar str = lpar ^ str ^ rpar;
    2.23  
    2.24  (*simple quoting (does not escape special chars)*)
    2.25 -val quote = parents "\"" "\"";
    2.26 +val quote = enclose "\"" "\"";
    2.27  
    2.28  (*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
    2.29  fun space_implode a bs = implode (separate a bs);