# HG changeset patch # User wenzelm # Date 1493760113 -7200 # Node ID 2229276a1f99cb599edf1cf51b33ef59231a2385 # Parent 74ec3cfcb6bfdc46cfd05691d78eea5409e6b89d eliminated redundant type SQL.View; eliminated unused DROP operations; diff -r 74ec3cfcb6bf -r 2229276a1f99 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Tue May 02 21:57:32 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Tue May 02 23:21:53 2017 +0200 @@ -897,17 +897,21 @@ /* full view on build_log data */ // WARNING: This may cause performance problems, e.g. with sqlitebrowser - val full_view: SQL.View = - SQL.View("isabelle_build_log", + val full_view: SQL.Table = + { + val columns = Meta_Info.table.columns ::: - Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)), - { - val table1 = Meta_Info.table - val table2 = Build_Info.sessions_table - SQL.select(Meta_Info.log_name(table1) :: full_view.columns.tail) + - SQL.join(table1, table2, - Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql) - }) + Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)) + SQL.Table("isabelle_build_log", columns, + view = + { + val table1 = Meta_Info.table + val table2 = Build_Info.sessions_table + SQL.select(Meta_Info.log_name(table1) :: columns.tail) + + SQL.join(table1, table2, + Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql) + }) + } /* main operations */ diff -r 74ec3cfcb6bf -r 2229276a1f99 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Tue May 02 21:57:32 2017 +0200 +++ b/src/Pure/General/sql.scala Tue May 02 23:21:53 2017 +0200 @@ -77,11 +77,6 @@ /* columns */ - trait Qualifier - { - def name: String - } - object Column { def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = @@ -103,8 +98,8 @@ sealed case class Column( name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false) { - def apply(qual: Qualifier): Column = - Column(Long_Name.qualify(qual.name, name), T, strict = strict, primary_key = primary_key) + def apply(table: Table): Column = + Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key) def sql: String = identifer(name) def sql_decl(sql_type: Type.Value => String): String = @@ -119,7 +114,7 @@ /* tables */ - sealed case class Table(name: String, columns: List[Column]) extends Qualifier + sealed case class Table(name: String, columns: List[Column], view: String = "") { private val columns_index: Map[String, Int] = columns.iterator.map(_.name).zipWithIndex.toMap @@ -129,6 +124,8 @@ case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name)) } + def is_view: Boolean = view != "" + def sql: String = identifer(name) def sql_columns(sql_type: Type.Value => String): String = @@ -145,9 +142,6 @@ "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + identifer(name) + " " + sql_columns(sql_type) - def sql_drop(strict: Boolean): String = - "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + identifer(name) - def sql_create_index( index_name: String, index_columns: List[Column], strict: Boolean, unique: Boolean): String = @@ -155,9 +149,6 @@ (if (strict) "" else "IF NOT EXISTS ") + identifer(index_name) + " ON " + identifer(name) + " " + enclosure(index_columns.map(_.name)) - def sql_drop_index(index_name: String, strict: Boolean): String = - "DROP INDEX " + (if (strict) "" else "IF EXISTS ") + identifer(index_name) - def sql_insert: String = "INSERT INTO " + identifer(name) + " VALUES " + enclosure(columns.map(_ => "?")) @@ -172,17 +163,6 @@ } - /* views */ - - sealed case class View(name: String, columns: List[Column], query: String) extends Qualifier - { - def sql: String = identifer(name) - def sql_create: String = "CREATE VIEW " + identifer(name) + " AS " + query - - override def toString: String = - "VIEW " + identifer(name) + " " + enclosure(columns.map(_.sql_decl(sql_type_default))) - } - /** SQL database operations **/ @@ -320,20 +300,18 @@ using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))( _.execute()) - def drop_table(table: Table, strict: Boolean = false): Unit = - using(statement(table.sql_drop(strict)))(_.execute()) - def create_index(table: Table, name: String, columns: List[Column], strict: Boolean = false, unique: Boolean = false): Unit = using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute()) - def drop_index(table: Table, name: String, strict: Boolean = false): Unit = - using(statement(table.sql_drop_index(name, strict)))(_.execute()) - - def create_view(view: View, strict: Boolean = false): Unit = - if (strict || !tables.contains(view.name)) { - using(statement(view.sql_create))(_.execute()) + def create_view(table: Table, strict: Boolean = false): Unit = + { + require(table.is_view) + if (strict || !tables.contains(table.name)) { + val sql = "CREATE VIEW " + identifer(table.name) + " AS " + table.view + using(statement(sql))(_.execute()) } + } } }