# HG changeset patch
# User wenzelm
# Date 1476558484 -7200
# Node ID 367d83d6030e038ae3f0b5dc96a4aa63454f39b0
# Parent  dbc8294c75d313b8a4158d38c89102cefcb65db7
clarified hg.id operation, with explicit tip as default;

diff -r dbc8294c75d3 -r 367d83d6030e src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 15 21:02:39 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 15 21:08:04 2016 +0200
@@ -140,7 +140,7 @@
     hg.update(rev = rev, clean = true)
     progress.echo_if(verbose, hg.log(rev, options = "-l1"))
 
-    val isabelle_version = hg.identify(rev, options = "-i")
+    val isabelle_version = hg.id(rev)
     val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
 
 
diff -r dbc8294c75d3 -r 367d83d6030e src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Sat Oct 15 21:02:39 2016 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Sat Oct 15 21:08:04 2016 +0200
@@ -72,7 +72,7 @@
 
 
   final def hg_id(path: Path): String =
-    Mercurial.repository(path).identify(options = "-i")
+    Mercurial.repository(path).id()
 
   final def print_section(title: String): Unit =
     println(s"\n=== $title ===\n")
diff -r dbc8294c75d3 -r 367d83d6030e src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 21:02:39 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 15 21:08:04 2016 +0200
@@ -35,10 +35,13 @@
   private val isabelle_identify =
     Logger_Task("isabelle_identify", logger =>
       {
-        val isabelle_id = Mercurial.repository(isabelle_repos).identify(options = "-i")
+        val isabelle_id = Mercurial.repository(isabelle_repos).id()
         val afp_id =
-          Mercurial.setup_repository(
-            logger.cronjob_options.string("afp_repos"), afp_repos).pull_id()
+        {
+          val hg = Mercurial.setup_repository(logger.cronjob_options.string("afp_repos"), afp_repos)
+          hg.pull()
+          hg.id()
+        }
 
         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
           terminate_lines(
@@ -258,7 +261,7 @@
     val main_start_date = Date.now()
     File.write(main_state_file, main_start_date + " " + log_service.hostname)
 
-    val rev = Mercurial.repository(isabelle_repos).identify(options = "-i")
+    val rev = Mercurial.repository(isabelle_repos).id()
 
     run(main_start_date,
       Logger_Task("isabelle_cronjob", _ =>
diff -r dbc8294c75d3 -r 367d83d6030e src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Oct 15 21:02:39 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Oct 15 21:08:04 2016 +0200
@@ -79,9 +79,11 @@
     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
       hg.command("heads", opt_template(template), options).check.out_lines
 
-    def identify(rev: String = "", options: String = ""): String =
+    def identify(rev: String = "tip", options: String = ""): String =
       hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
 
+    def id(rev: String = "tip"): String = identify(rev, options = "-i")
+
     def manifest(rev: String = "", options: String = ""): List[String] =
       hg.command("manifest", opt_rev(rev), options).check.out_lines
 
@@ -91,12 +93,6 @@
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
       hg.command("pull", opt_rev(rev) + optional(remote), options).check
 
-    def pull_id(remote: String = ""): String =
-    {
-      hg.pull(remote = remote, options = "-q")
-      hg.identify("tip", options = "-i")
-    }
-
     def update(
       rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
     {