tuned queries;
authorwenzelm
Sat May 19 20:19:15 2018 +0200 (14 months ago)
changeset 682223c1a716e7f59
parent 68221 dbef88c2b6c5
child 68223 88dd06301dd3
tuned queries;
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export.scala	Sat May 19 20:05:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Sat May 19 20:19:15 2018 +0200
     1.3 @@ -46,7 +46,15 @@
     1.4        stmt.execute_query().iterator(res => res.string(Data.name)).toList)
     1.5    }
     1.6  
     1.7 -  def read_theory_names(db: SQL.Database, session_name: String): List[(String, String)] =
     1.8 +  def read_theory_names(db: SQL.Database, session_name: String): List[String] =
     1.9 +  {
    1.10 +    val select =
    1.11 +      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
    1.12 +    db.using_statement(select)(stmt =>
    1.13 +      stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
    1.14 +  }
    1.15 +
    1.16 +  def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
    1.17    {
    1.18      val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
    1.19      db.using_statement(select)(stmt =>
    1.20 @@ -255,7 +263,7 @@
    1.21      using(store.open_database(session_name))(db =>
    1.22      {
    1.23        db.transaction {
    1.24 -        val export_names = read_theory_names(db, session_name)
    1.25 +        val export_names = read_theory_exports(db, session_name)
    1.26  
    1.27          // list
    1.28          if (export_list) {
     2.1 --- a/src/Pure/Thy/export_theory.scala	Sat May 19 20:05:13 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Sat May 19 20:19:15 2018 +0200
     2.3 @@ -32,9 +32,8 @@
     2.4        using(store.open_database(session_name))(db =>
     2.5        {
     2.6          db.transaction {
     2.7 -          Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.
     2.8 -            map((theory_name: String) =>
     2.9 -              read_theory(db, session_name, theory_name, types = types, consts = consts)).toList
    2.10 +          Export.read_theory_names(db, session_name).map((theory_name: String) =>
    2.11 +            read_theory(db, session_name, theory_name, types = types, consts = consts))
    2.12          }
    2.13        })
    2.14