385 val hierarchy = deps.sessions_structure.hierarchy(session) |
387 val hierarchy = deps.sessions_structure.hierarchy(session) |
386 val info = deps.sessions_structure(session) |
388 val info = deps.sessions_structure(session) |
387 val options = info.options |
389 val options = info.options |
388 val base = deps(session) |
390 val base = deps(session) |
389 |
391 |
|
392 def make_session_dir(name: String): Path = |
|
393 Isabelle_System.make_directory( |
|
394 presentation.dir(db_context.store, deps.sessions_structure(name))) |
|
395 |
|
396 val session_dir = make_session_dir(session) |
390 val presentation_dir = presentation.dir(db_context.store) |
397 val presentation_dir = presentation.dir(db_context.store) |
391 val session_dir = Isabelle_System.make_directory(presentation.dir(db_context.store, info)) |
|
392 |
398 |
393 Bytes.write(session_dir + session_graph_path, |
399 Bytes.write(session_dir + session_graph_path, |
394 graphview.Graph_File.make_pdf(options, base.session_graph_display)) |
400 graphview.Graph_File.make_pdf(options, base.session_graph_display)) |
395 |
401 |
396 val documents = |
402 val documents = |
421 Library.separate(HTML.break ::: HTML.nl, |
427 Library.separate(HTML.break ::: HTML.nl, |
422 (deps_link :: readme_links ::: document_links). |
428 (deps_link :: readme_links ::: document_links). |
423 map(link => HTML.text("View ") ::: List(link))).flatten |
429 map(link => HTML.text("View ") ::: List(link))).flatten |
424 } |
430 } |
425 |
431 |
|
432 val theory_exports0: Set[String] = html_context.cached_theories |
426 val theory_exports: Map[String, Export_Theory.Theory] = |
433 val theory_exports: Map[String, Export_Theory.Theory] = |
427 (for ((_, entry) <- base.known_theories.iterator) yield { |
434 (for ((_, entry) <- base.known_theories.iterator) yield { |
428 val thy_name = entry.name.theory |
435 val thy_name = entry.name.theory |
429 val theory = |
436 val theory = |
430 if (thy_name == Thy_Header.PURE) Export_Theory.no_theory |
437 if (thy_name == Thy_Header.PURE) Export_Theory.no_theory |
439 thy_name -> theory |
446 thy_name -> theory |
440 }).toMap |
447 }).toMap |
441 |
448 |
442 val theories: List[XML.Body] = |
449 val theories: List[XML.Body] = |
443 { |
450 { |
444 var seen_files = List.empty[(Path, String, Document.Node.Name)] |
451 sealed case class Seen_File( |
|
452 src_path: Path, file_name: String, thy_session: String, thy_name: Document.Node.Name) |
|
453 { |
|
454 def check(src_path1: Path, file_name1: String, thy_session1: String): Boolean = |
|
455 (src_path == src_path1 || file_name == file_name1) && thy_session == thy_session1 |
|
456 } |
|
457 var seen_files = List.empty[Seen_File] |
445 |
458 |
446 def node_file(node: Document.Node.Name): String = |
459 def node_file(node: Document.Node.Name): String = |
447 if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node)) |
460 if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node)) |
448 |
461 |
449 def entity_anchor( |
462 def entity_anchor( |
547 |
560 |
548 Theory(name, command, files_html, html) |
561 Theory(name, command, files_html, html) |
549 } |
562 } |
550 } |
563 } |
551 |
564 |
552 for (thy <- Par_List.map(read_theory, base.session_theories).flatten) |
565 val present_theories = |
553 yield { |
566 for ((name, _) <- base.used_theories if !theory_exports0.contains(name.theory)) |
|
567 yield name |
|
568 |
|
569 (for (thy <- Par_List.map(read_theory, present_theories).flatten) yield { |
|
570 val thy_session = base.theory_qualifier(thy.name) |
|
571 val thy_dir = make_session_dir(thy_session) |
554 val files = |
572 val files = |
555 for { (src_path, file_html) <- thy.files_html } |
573 for { (src_path, file_html) <- thy.files_html } |
556 yield { |
574 yield { |
557 val file_name = html_path(src_path) |
575 val file_name = html_path(src_path) |
558 |
576 |
559 seen_files.find(p => p._1 == src_path || p._2 == file_name) match { |
577 seen_files.find(_.check(src_path, file_name, thy_session)) match { |
560 case None => seen_files ::= (src_path, file_name, thy.name) |
578 case None => seen_files ::= Seen_File(src_path, file_name, thy_session, thy.name) |
561 case Some((_, _, thy_name1)) => |
579 case Some(seen_file) => |
562 error("Incoherent use of file name " + src_path + " as " + quote(file_name) + |
580 error("Incoherent use of file name " + src_path + " as " + quote(file_name) + |
563 " in theory " + thy_name1 + " vs. " + thy.name) |
581 " in theory " + seen_file.thy_name + " vs. " + thy.name) |
564 } |
582 } |
565 |
583 |
566 val file_path = session_dir + Path.explode(file_name) |
584 val file_path = thy_dir + Path.explode(file_name) |
567 val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) |
585 val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) |
568 HTML.write_document(file_path.dir, file_path.file_name, |
586 HTML.write_document(file_path.dir, file_path.file_name, |
569 List(HTML.title(file_title)), List(html_context.head(file_title), file_html), |
587 List(HTML.title(file_title)), List(html_context.head(file_title), file_html), |
570 base = Some(presentation_dir)) |
588 base = Some(presentation_dir)) |
571 |
589 |
572 List(HTML.link(file_name, HTML.text(file_title))) |
590 List(HTML.link(file_name, HTML.text(file_title))) |
573 } |
591 } |
574 |
592 |
575 val thy_title = "Theory " + thy.name.theory_base_name |
593 val thy_title = "Theory " + thy.name.theory_base_name |
576 |
594 |
577 HTML.write_document(session_dir, html_name(thy.name), |
595 HTML.write_document(thy_dir, html_name(thy.name), |
578 List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html), |
596 List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html), |
579 base = Some(presentation_dir)) |
597 base = Some(presentation_dir)) |
580 |
598 |
581 List(HTML.link(html_name(thy.name), |
599 if (thy_session == session) { |
582 HTML.text(thy.name.theory_base_name) ::: |
600 Some( |
583 (if (files.isEmpty) Nil else List(HTML.itemize(files))))) |
601 List(HTML.link(html_name(thy.name), |
584 } |
602 HTML.text(thy.name.theory_base_name) ::: |
|
603 (if (files.isEmpty) Nil else List(HTML.itemize(files)))))) |
|
604 } |
|
605 else None |
|
606 }).flatten |
585 } |
607 } |
586 |
608 |
587 val title = "Session " + session |
609 val title = "Session " + session |
588 HTML.write_document(session_dir, "index.html", |
610 HTML.write_document(session_dir, "index.html", |
589 List(HTML.title(title + Isabelle_System.isabelle_heading())), |
611 List(HTML.title(title + Isabelle_System.isabelle_heading())), |