tuned;
authorwenzelm
Fri Sep 07 17:03:58 2018 +0200 (9 months ago)
changeset 68924feed46aa1969
parent 68923 59d2eab3f8b9
child 68925 76ce16eefab9
tuned;
src/Pure/Thy/export.scala
     1.1 --- a/src/Pure/Thy/export.scala	Fri Sep 07 14:07:34 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Fri Sep 07 17:03:58 2018 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5    class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
     1.6    {
     1.7 -    private val export_errors = Synchronized[List[String]](Nil)
     1.8 +    private val errors = Synchronized[List[String]](Nil)
     1.9  
    1.10      private val consumer =
    1.11        Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
    1.12 @@ -175,8 +175,8 @@
    1.13            entry.body.join
    1.14            db.transaction {
    1.15              if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
    1.16 -              val err = message("Duplicate export", entry.theory_name, entry.name)
    1.17 -              export_errors.change(errs => err :: errs)
    1.18 +              val msg = message("Duplicate export", entry.theory_name, entry.name)
    1.19 +              errors.change(msg :: _)
    1.20              }
    1.21              else entry.write(db)
    1.22            }
    1.23 @@ -190,7 +190,7 @@
    1.24      {
    1.25        consumer.shutdown()
    1.26        if (close) db.close()
    1.27 -      export_errors.value.reverse
    1.28 +      errors.value.reverse
    1.29      }
    1.30    }
    1.31