equal
deleted
inserted
replaced
66 |
66 |
67 /* presentation state */ |
67 /* presentation state */ |
68 |
68 |
69 class State |
69 class State |
70 { |
70 { |
71 /* already presented theories */ |
|
72 |
|
73 private val already_presented = Synchronized(Set.empty[String]) |
|
74 |
|
75 def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] = |
|
76 already_presented.change_result(presented => |
|
77 (nodes.filterNot(name => presented.contains(name.theory)), |
|
78 presented ++ nodes.iterator.map(_.theory))) |
|
79 |
|
80 |
|
81 /* cached theory exports */ |
71 /* cached theory exports */ |
82 |
72 |
83 val cache: Term.Cache = Term.Cache.make() |
73 val cache: Term.Cache = Term.Cache.make() |
84 |
74 |
85 private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory]) |
75 private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory]) |
653 } |
643 } |
654 else None |
644 else None |
655 }) |
645 }) |
656 } |
646 } |
657 |
647 |
658 val theories = state.register_presented(hierarchy_theories).flatMap(present_theory) |
648 val theories = base.session_theories.flatMap(present_theory) |
659 |
649 |
660 val title = "Session " + session |
650 val title = "Session " + session |
661 HTML.write_document(session_dir, "index.html", |
651 HTML.write_document(session_dir, "index.html", |
662 List(HTML.title(title + Isabelle_System.isabelle_heading())), |
652 List(HTML.title(title + Isabelle_System.isabelle_heading())), |
663 html_context.head(title, List(HTML.par(view_links))) :: |
653 html_context.head(title, List(HTML.par(view_links))) :: |