# HG changeset patch
# User wenzelm
# Date 1507922431 -7200
# Node ID f8f42289c4dfc9266501173bbc7ca89556073a24
# Parent  6b90c688a6dc089de7bdc8f02d9b9c0b0c6f2303
tuned signature;

diff -r 6b90c688a6dc -r f8f42289c4df src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Oct 13 21:15:04 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Oct 13 21:20:31 2017 +0200
@@ -652,8 +652,8 @@
 
     /* main content */
 
-    val log_name = SQL.Column.string("log_name", primary_key = true)
-    val session_name = SQL.Column.string("session_name", primary_key = true)
+    val log_name = SQL.Column.string("log_name").make_primary_key
+    val session_name = SQL.Column.string("session_name").make_primary_key
     val chapter = SQL.Column.string("chapter")
     val groups = SQL.Column.string("groups")
     val threads = SQL.Column.int("threads")
@@ -690,7 +690,7 @@
     {
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
-      build_log_table("isabelle_afp_versions", List(version1.copy(primary_key = true), version2),
+      build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
         SQL.select(List(version1, version2), distinct = true) + meta_info_table +
         " WHERE " + version1.defined + " AND " + version2.defined)
     }
@@ -703,7 +703,7 @@
     val pull_date_table: SQL.Table =
     {
       val version = Prop.isabelle_version
-      build_log_table("pull_date", List(version.copy(primary_key = true), pull_date),
+      build_log_table("pull_date", List(version.make_primary_key, pull_date),
         "SELECT " + version + ", min(" + Prop.build_start + ") AS " + pull_date +
         " FROM " + meta_info_table +
         " WHERE " + version.defined + " AND " + Prop.build_start.defined +
@@ -716,7 +716,7 @@
       val version2 = Prop.afp_version
       val table1 = pull_date_table
       val table2 = isabelle_afp_versions_table
-      build_log_table("afp_pull_date", List(version1.copy(primary_key = true), version2, pull_date),
+      build_log_table("afp_pull_date", List(version1.make_primary_key, version2, pull_date),
         table1.select(List(version1(table1), version2(table2), pull_date(table1))) +
         SQL.join_inner + table2.query_named + " ON " + version1(table1) + " = " + version1(table2))
     }
diff -r 6b90c688a6dc -r f8f42289c4df src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Oct 13 21:15:04 2017 +0200
+++ b/src/Pure/General/sql.scala	Fri Oct 13 21:20:31 2017 +0200
@@ -105,6 +105,8 @@
     name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false,
     expr: SQL.Source = "")
   {
+    def make_primary_key: Column = copy(primary_key = true)
+
     def apply(table: Table): Column =
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
diff -r 6b90c688a6dc -r f8f42289c4df src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Oct 13 21:15:04 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Oct 13 21:20:31 2017 +0200
@@ -824,7 +824,7 @@
 
   object Session_Info
   {
-    val session_name = SQL.Column.string("session_name", primary_key = true)
+    val session_name = SQL.Column.string("session_name").make_primary_key
 
     // Build_Log.Session_Info
     val session_timing = SQL.Column.bytes("session_timing")
diff -r 6b90c688a6dc -r f8f42289c4df src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Oct 13 21:15:04 2017 +0200
+++ b/src/Pure/Tools/server.scala	Fri Oct 13 21:20:31 2017 +0200
@@ -20,7 +20,7 @@
   {
     val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
 
-    val name = SQL.Column.string("name", primary_key = true)
+    val name = SQL.Column.string("name").make_primary_key
     val port = SQL.Column.int("port")
     val password = SQL.Column.string("password")
     val table = SQL.Table("isabelle_servers", List(name, port, password))