src/Pure/Thy/presentation.scala
changeset 72665 7e5102e11c5e
parent 72663 e9030100f97d
child 72669 5e7916535860
equal deleted inserted replaced
72664:0d3224b3a92c 72665:7e5102e11c5e
   434     val documents =
   434     val documents =
   435       for (doc <- info.documents)
   435       for (doc <- info.documents)
   436       yield {
   436       yield {
   437         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
   437         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
   438         {
   438         {
       
   439           progress.echo_document("Building document " + session + "/" + doc.name + " ...")
       
   440           val start = Time.now()
       
   441 
       
   442 
   439           // prepare sources
   443           // prepare sources
   440 
   444 
   441           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
   445           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
   442           val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
   446           val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
   443           val sources = SHA1.digest_set(digests).toString
   447           val sources = SHA1.digest_set(digests).toString
   501                 "Failed to build document " + quote(doc.name))
   505                 "Failed to build document " + quote(doc.name))
   502             }
   506             }
   503             else if (!result_path.is_file) {
   507             else if (!result_path.is_file) {
   504               error("Bad document result: expected to find " + root_pdf)
   508               error("Bad document result: expected to find " + root_pdf)
   505             }
   509             }
   506             else doc.set_sources(sources) -> Bytes.read(result_path)
   510             else {
       
   511               val stop = Time.now()
       
   512               val timing = stop - start
       
   513               progress.echo_document("Finished document " + session + "/" + doc.name +
       
   514                 " (" + timing.message_hms + " elapsed time)")
       
   515 
       
   516               doc.set_sources(sources) -> Bytes.read(result_path)
       
   517             }
   507           }
   518           }
   508         })
   519         })
   509       }
   520       }
   510 
   521 
   511     for (dir <- doc_output; (doc, pdf) <- documents) {
   522     for (dir <- doc_output; (doc, pdf) <- documents) {