equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
|
10 import java.util.Locale |
10 import java.time.{Instant, ZonedDateTime, ZoneId} |
11 import java.time.{Instant, ZonedDateTime, ZoneId} |
11 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
12 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
12 import java.time.temporal.TemporalAccessor |
13 import java.time.temporal.TemporalAccessor |
13 |
14 |
14 import scala.annotation.tailrec |
15 import scala.annotation.tailrec |
39 def parse(str: String): Date = |
40 def parse(str: String): Date = |
40 new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str)))) |
41 new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str)))) |
41 } |
42 } |
42 } |
43 } |
43 |
44 |
44 def make_patterns(patterns: List[String], filter: String => String = s => s): Format = |
45 def make_variants(patterns: List[String], |
45 make(patterns.toList.map(DateTimeFormatter.ofPattern(_)), filter) |
46 locales: List[Locale] = List(Locale.ROOT), |
|
47 filter: String => String = s => s): Format = |
|
48 { |
|
49 val fmts = |
|
50 patterns.flatMap(pat => |
|
51 { |
|
52 val fmt = DateTimeFormatter.ofPattern(pat) |
|
53 locales.map(fmt.withLocale(_)) |
|
54 }) |
|
55 make(fmts, filter) |
|
56 } |
46 |
57 |
47 def apply(patterns: String*): Format = |
58 def apply(patterns: String*): Format = |
48 make(patterns.toList.map(DateTimeFormatter.ofPattern(_))) |
59 make(patterns.toList.map(DateTimeFormatter.ofPattern(_))) |
49 |
60 |
50 val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx") |
61 val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx") |