--- a/src/Pure/library.ML Tue Jun 14 20:48:41 2016 +0200
+++ b/src/Pure/library.ML Tue Jun 14 20:48:42 2016 +0200
@@ -146,6 +146,7 @@
val trim_line: string -> string
val replicate_string: int -> string -> string
val translate_string: (string -> string) -> string -> string
+ val align_right: string -> int -> string -> string
val match_string: string -> string -> bool
(*reals*)
@@ -720,6 +721,12 @@
fun translate_string f = String.translate (f o String.str);
+fun align_right c k s =
+ let
+ val _ = if size c <> 1 orelse size s > k
+ then raise Fail "align_right" else ()
+ in replicate_string (k - size s) c ^ s end;
+
(*crude matching of str against simple glob pat*)
fun match_string pat str =
let