equal
deleted
inserted
replaced
50 Par_List.map[(String, String), Option[String]]( |
50 Par_List.map[(String, String), Option[String]]( |
51 { |
51 { |
52 case (doc, session) => |
52 case (doc, session) => |
53 try { |
53 try { |
54 progress.echo("Documentation " + doc + " ...") |
54 progress.echo("Documentation " + doc + " ...") |
55 Presentation.build_documents(session, deps, store, |
55 |
56 output_pdf = Some(Path.explode("~~/src/doc"))) |
56 using(store.open_database_context(deps.sessions_structure))(db_context => |
|
57 Presentation.build_documents(session, deps, db_context, |
|
58 output_pdf = Some(Path.explode("~~/src/doc")))) |
57 None |
59 None |
58 } |
60 } |
59 catch { |
61 catch { |
60 case Exn.Interrupt.ERROR(msg) => |
62 case Exn.Interrupt.ERROR(msg) => |
61 val sep = if (msg.contains('\n')) "\n" else " " |
63 val sep = if (msg.contains('\n')) "\n" else " " |