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.io.{File => JFile} |
11 import java.io.{File => JFile} |
11 import java.time.ZonedDateTime |
12 import java.time.ZonedDateTime |
12 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
13 import java.time.format.{DateTimeFormatter, DateTimeParseException} |
13 |
14 |
14 import scala.collection.mutable |
15 import scala.collection.mutable |
180 |
181 |
181 |
182 |
182 /* header and meta data */ |
183 /* header and meta data */ |
183 |
184 |
184 val Date_Format = |
185 val Date_Format = |
185 Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), |
186 Date.Format.make_variants( |
|
187 List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), |
|
188 List(Locale.ENGLISH, Locale.GERMAN), |
186 // workaround for jdk-8u102 |
189 // workaround for jdk-8u102 |
187 s => Word.implode(Word.explode(s).map({ |
190 s => Word.implode(Word.explode(s).map({ |
188 case "CET" | "MET" => "GMT+1" |
191 case "CET" | "MET" => "GMT+1" |
189 case "CEST" | "MEST" => "GMT+2" |
192 case "CEST" | "MEST" => "GMT+2" |
190 case "EST" => "GMT+1" // FIXME ?? |
193 case "EST" => "GMT+1" // FIXME ?? |