equal
deleted
inserted
replaced
41 }) |
41 }) |
42 } |
42 } |
43 |
43 |
44 def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) = |
44 def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) = |
45 { |
45 { |
46 val label = "Preview " + quote(model.node_name.toString) |
46 val label = "Preview " + quote(model.node_name.theory_base_name) |
47 val content = |
47 val content = |
48 HTML.output_document( |
48 HTML.output_document( |
49 List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)), |
49 List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)), |
50 List( |
50 List(HTML.source(Present.theory_document(snapshot))), |
51 HTML.chapter("Theory " + quote(model.node_name.theory_base_name)), |
|
52 HTML.source(Present.theory_document(snapshot))), |
|
53 css = "") |
51 css = "") |
54 (label, content) |
52 (label, content) |
55 } |
53 } |
56 } |
54 } |