src/Pure/Thy/export.scala
changeset 71726 a5fda30edae2
parent 71624 f0499449e149
child 71939 107472ccc60d
equal deleted inserted replaced
71725:c255ed582095 71726:a5fda30edae2
   297 
   297 
   298   def export_files(
   298   def export_files(
   299     store: Sessions.Store,
   299     store: Sessions.Store,
   300     session_name: String,
   300     session_name: String,
   301     export_dir: Path,
   301     export_dir: Path,
   302     progress: Progress = No_Progress,
   302     progress: Progress = new Progress,
   303     export_prune: Int = 0,
   303     export_prune: Int = 0,
   304     export_list: Boolean = false,
   304     export_list: Boolean = false,
   305     export_patterns: List[String] = Nil)
   305     export_patterns: List[String] = Nil)
   306   {
   306   {
   307     using(store.open_database(session_name))(db =>
   307     using(store.open_database(session_name))(db =>