4 Theory presentation: HTML and PDF-LaTeX documents. |
4 Theory presentation: HTML and PDF-LaTeX documents. |
5 *) |
5 *) |
6 |
6 |
7 signature PRESENT = |
7 signature PRESENT = |
8 sig |
8 sig |
9 val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit |
9 val init: bool -> Path.T -> string list -> string * string -> bool -> unit |
10 val finish: unit -> unit |
10 val finish: unit -> unit |
11 val begin_theory: int -> (unit -> HTML.text) -> theory -> theory |
11 val begin_theory: int -> HTML.text -> theory -> theory |
12 end; |
12 end; |
13 |
13 |
14 structure Present: PRESENT = |
14 structure Present: PRESENT = |
15 struct |
15 struct |
16 |
16 |
59 (** global session state **) |
59 (** global session state **) |
60 |
60 |
61 (* session_info *) |
61 (* session_info *) |
62 |
62 |
63 type session_info = |
63 type session_info = |
64 {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool, |
64 {name: string, chapter: string, info_path: Path.T, info: bool, |
65 verbose: bool, readme: Path.T option}; |
65 verbose: bool, readme: Path.T option}; |
66 |
66 |
67 fun make_session_info |
67 fun make_session_info (name, chapter, info_path, info, verbose, readme) = |
68 (symbols, name, chapter, info_path, info, verbose, readme) = |
68 {name = name, chapter = chapter, info_path = info_path, info = info, |
69 {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info, |
|
70 verbose = verbose, readme = readme}: session_info; |
69 verbose = verbose, readme = readme}: session_info; |
71 |
70 |
72 |
71 |
73 (* state *) |
72 (* state *) |
74 |
73 |
86 |
85 |
87 (** document preparation **) |
86 (** document preparation **) |
88 |
87 |
89 (* init session *) |
88 (* init session *) |
90 |
89 |
91 fun init symbols info info_path documents (chapter, name) verbose = |
90 fun init info info_path documents (chapter, name) verbose = |
92 let |
91 let |
93 val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; |
92 val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; |
94 |
93 val symbols = Resources.html_symbols (); |
95 val docs = |
94 val docs = |
96 (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
95 (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
97 map (fn name => (Url.File (document_path name), name)) documents; |
96 map (fn name => (Url.File (document_path name), name)) documents; |
98 in |
97 in |
99 session_info := |
98 session_info := SOME (make_session_info (name, chapter, info_path, info, verbose, readme)); |
100 SOME (make_session_info (symbols, name, chapter, info_path, info, verbose, readme)); |
|
101 Synchronized.change browser_info (K empty_browser_info); |
99 Synchronized.change browser_info (K empty_browser_info); |
102 add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) |
100 add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs) |
103 end; |
101 end; |
104 |
102 |
105 |
103 |
146 SOME (Path.parent + Path.basic session + link) |
144 SOME (Path.parent + Path.basic session + link) |
147 else if chapter = Context.PureN then NONE |
145 else if chapter = Context.PureN then NONE |
148 else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) |
146 else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link) |
149 end; |
147 end; |
150 |
148 |
151 fun begin_theory update_time mk_text thy = |
149 fun begin_theory update_time html thy = |
152 with_session_info thy (fn {symbols, name = session_name, chapter, ...} => |
150 with_session_info thy (fn {name = session_name, chapter, ...} => |
153 let |
151 let |
154 val name = Context.theory_name thy; |
152 val name = Context.theory_name thy; |
155 |
153 |
156 val parent_specs = |
154 val parent_specs = |
157 Theory.parents_of thy |> map (fn parent => |
155 Theory.parents_of thy |> map (fn parent => |
158 (Option.map Url.File (theory_link (chapter, session_name) parent), |
156 (Option.map Url.File (theory_link (chapter, session_name) parent), |
159 (Context.theory_name parent))); |
157 (Context.theory_name parent))); |
160 |
158 |
161 val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ())); |
159 val symbols = Resources.html_symbols (); |
|
160 val _ = update_html name (HTML.theory symbols name parent_specs html); |
162 |
161 |
163 val _ = |
162 val _ = |
164 if is_session_theory thy then |
163 if is_session_theory thy then |
165 add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)) |
164 add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name)) |
166 else (); |
165 else (); |