# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1474037353 -7200
# Node ID 7534eec7cfadf51a249aff2b2fa6638ca3f3bded
# Parent  c181a84eb6de3af56182e769fd498dd4aafb3d18
benchmark doesn't need to build documents

diff -r c181a84eb6de -r 7534eec7cfad Admin/jenkins/build/ci_build_benchmark.scala
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Fri Sep 16 16:48:59 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Sep 16 16:49:13 2016 +0200
@@ -3,6 +3,7 @@
 
   import isabelle._
 
+  override def documents = false
   def threads = 6
   def jobs = 1
   def include = Nil
diff -r c181a84eb6de -r 7534eec7cfad src/Pure/Tools/ci_profile.scala
--- a/src/Pure/Tools/ci_profile.scala	Fri Sep 16 16:48:59 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Fri Sep 16 16:49:13 2016 +0200
@@ -59,6 +59,17 @@
     (Timing.zero /: timings)(_ + _)
   }
 
+  private def with_documents(options: Options): Options =
+  {
+    if (documents)
+      options
+        .bool.update("browser_info", true)
+        .string.update("document", "pdf")
+        .string.update("document_variants", "document:outline=/proof,/ML")
+    else
+      options
+  }
+
 
   final def hg_id(path: Path): String =
     Isabelle_System.hg("id -i", path.file).out
@@ -80,10 +91,7 @@
     System.getProperties().putAll(props)
 
     val options =
-      Options.init()
-        .bool.update("browser_info", true)
-        .string.update("document", "pdf")
-        .string.update("document_variants", "document:outline=/proof,/ML")
+      with_documents(Options.init())
         .int.update("parallel_proofs", 2)
         .int.update("threads", threads)
 
@@ -127,6 +135,8 @@
 
   /* profile */
 
+  def documents: Boolean = true
+
   def threads: Int
   def jobs: Int
   def include: List[Path]