equal
deleted
inserted
replaced
396 val image_width_stretch = (image_width * data_entry.stretch).toInt |
396 val image_width_stretch = (image_width * data_entry.stretch).toInt |
397 |
397 |
398 progress.echo("output " + quote(data_name)) |
398 progress.echo("output " + quote(data_name)) |
399 |
399 |
400 val dir = target_dir + Path.basic(clean_name(data_name)) |
400 val dir = target_dir + Path.basic(clean_name(data_name)) |
401 Isabelle_System.mkdirs(dir) |
401 Isabelle_System.make_directory(dir) |
402 |
402 |
403 val data_files = |
403 val data_files = |
404 (for (session <- data_entry.sessions) yield { |
404 (for (session <- data_entry.sessions) yield { |
405 val csv_file = session.make_csv |
405 val csv_file = session.make_csv |
406 csv_file.write(dir) |
406 csv_file.write(dir) |