tuned signature;
authorwenzelm
Fri Oct 13 21:20:31 2017 +0200 (20 months ago)
changeset 66857f8f42289c4df
parent 66856 6b90c688a6dc
child 66858 2ca6f0275de7
tuned signature;
src/Pure/Admin/build_log.scala
src/Pure/General/sql.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Fri Oct 13 21:15:04 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Fri Oct 13 21:20:31 2017 +0200
     1.3 @@ -652,8 +652,8 @@
     1.4  
     1.5      /* main content */
     1.6  
     1.7 -    val log_name = SQL.Column.string("log_name", primary_key = true)
     1.8 -    val session_name = SQL.Column.string("session_name", primary_key = true)
     1.9 +    val log_name = SQL.Column.string("log_name").make_primary_key
    1.10 +    val session_name = SQL.Column.string("session_name").make_primary_key
    1.11      val chapter = SQL.Column.string("chapter")
    1.12      val groups = SQL.Column.string("groups")
    1.13      val threads = SQL.Column.int("threads")
    1.14 @@ -690,7 +690,7 @@
    1.15      {
    1.16        val version1 = Prop.isabelle_version
    1.17        val version2 = Prop.afp_version
    1.18 -      build_log_table("isabelle_afp_versions", List(version1.copy(primary_key = true), version2),
    1.19 +      build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
    1.20          SQL.select(List(version1, version2), distinct = true) + meta_info_table +
    1.21          " WHERE " + version1.defined + " AND " + version2.defined)
    1.22      }
    1.23 @@ -703,7 +703,7 @@
    1.24      val pull_date_table: SQL.Table =
    1.25      {
    1.26        val version = Prop.isabelle_version
    1.27 -      build_log_table("pull_date", List(version.copy(primary_key = true), pull_date),
    1.28 +      build_log_table("pull_date", List(version.make_primary_key, pull_date),
    1.29          "SELECT " + version + ", min(" + Prop.build_start + ") AS " + pull_date +
    1.30          " FROM " + meta_info_table +
    1.31          " WHERE " + version.defined + " AND " + Prop.build_start.defined +
    1.32 @@ -716,7 +716,7 @@
    1.33        val version2 = Prop.afp_version
    1.34        val table1 = pull_date_table
    1.35        val table2 = isabelle_afp_versions_table
    1.36 -      build_log_table("afp_pull_date", List(version1.copy(primary_key = true), version2, pull_date),
    1.37 +      build_log_table("afp_pull_date", List(version1.make_primary_key, version2, pull_date),
    1.38          table1.select(List(version1(table1), version2(table2), pull_date(table1))) +
    1.39          SQL.join_inner + table2.query_named + " ON " + version1(table1) + " = " + version1(table2))
    1.40      }
     2.1 --- a/src/Pure/General/sql.scala	Fri Oct 13 21:15:04 2017 +0200
     2.2 +++ b/src/Pure/General/sql.scala	Fri Oct 13 21:20:31 2017 +0200
     2.3 @@ -105,6 +105,8 @@
     2.4      name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false,
     2.5      expr: SQL.Source = "")
     2.6    {
     2.7 +    def make_primary_key: Column = copy(primary_key = true)
     2.8 +
     2.9      def apply(table: Table): Column =
    2.10        Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
    2.11  
     3.1 --- a/src/Pure/Thy/sessions.scala	Fri Oct 13 21:15:04 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Fri Oct 13 21:20:31 2017 +0200
     3.3 @@ -824,7 +824,7 @@
     3.4  
     3.5    object Session_Info
     3.6    {
     3.7 -    val session_name = SQL.Column.string("session_name", primary_key = true)
     3.8 +    val session_name = SQL.Column.string("session_name").make_primary_key
     3.9  
    3.10      // Build_Log.Session_Info
    3.11      val session_timing = SQL.Column.bytes("session_timing")
     4.1 --- a/src/Pure/Tools/server.scala	Fri Oct 13 21:15:04 2017 +0200
     4.2 +++ b/src/Pure/Tools/server.scala	Fri Oct 13 21:20:31 2017 +0200
     4.3 @@ -20,7 +20,7 @@
     4.4    {
     4.5      val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
     4.6  
     4.7 -    val name = SQL.Column.string("name", primary_key = true)
     4.8 +    val name = SQL.Column.string("name").make_primary_key
     4.9      val port = SQL.Column.int("port")
    4.10      val password = SQL.Column.string("password")
    4.11      val table = SQL.Table("isabelle_servers", List(name, port, password))