309 def update_root(): Unit = synchronized { |
309 def update_root(): Unit = synchronized { |
310 Meta_Data.init_directory(root_dir) |
310 Meta_Data.init_directory(root_dir) |
311 HTML.init_fonts(root_dir) |
311 HTML.init_fonts(root_dir) |
312 Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), |
312 Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), |
313 root_dir + Path.explode("isabelle.gif")) |
313 root_dir + Path.explode("isabelle.gif")) |
314 val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" |
314 |
315 File.write(root_dir + Path.explode("index.html"), |
315 Meta_Data.change(root_dir, Meta_Data.INDEX) { text => |
316 HTML.header + |
316 val index0 = Meta_Data.Index.parse(text, "root") |
317 """ |
317 val index = { |
318 <head> |
318 val items1 = |
319 """ + HTML.head_meta + """ |
319 for (entry <- sessions_structure.chapter_defs.list) |
320 <title>""" + title + """</title> |
320 yield Meta_Data.Item(entry.name, description = entry.description) |
321 </head> |
321 val items2 = |
322 |
322 (for { |
323 <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040"> |
323 (name, _) <- sessions_structure.chapters.iterator |
324 <center> |
324 if !items1.exists(_.name == name) |
325 <table width="100%" border="0" cellspacing="10" cellpadding="0"> |
325 } yield Meta_Data.Item(name)).toList |
326 <tr> |
326 (items1 ::: items2).foldLeft(index0)(_ + _) |
327 <td width="20%" valign="middle" align="center"><a href="https://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td> |
327 } |
328 |
328 val chapters = index.items |
329 <td width="80%" valign="middle" align="center"> |
329 |
330 <table width="90%" border="0" cellspacing="0" cellpadding="20"> |
330 if (index != index0) { |
331 <tr> |
331 val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" |
332 <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">""" + title + """</font></td> |
332 HTML.write_document(root_dir, "index.html", |
333 </tr> |
333 List(HTML.title(title + Isabelle_System.isabelle_heading())), |
334 </table> |
334 HTML.chapter(title) :: |
335 </td> |
335 (if (chapters.isEmpty) Nil |
336 </tr> |
336 else |
337 </table> |
337 List(HTML.div("sessions", |
338 </center> |
338 List(HTML.description( |
339 <hr /> |
339 chapters.map(chapter => |
340 """ + File.read(Path.explode("~~/lib/html/library_index_content.template")) + |
340 (List(HTML.link(chapter.name + "/index.html", HTML.text(chapter.name))), |
341 """ |
341 if (chapter.description.isEmpty) Nil |
342 </body> |
342 else HTML.break ::: List(HTML.pre(HTML.text(chapter.description)))))))))), |
343 """ + HTML.footer) |
343 root = Some(root_dir)) |
|
344 } |
|
345 |
|
346 index.print_json |
|
347 } |
344 } |
348 } |
345 } |
349 } |
346 |
350 |
347 sealed case class HTML_Document(title: String, content: String) |
351 sealed case class HTML_Document(title: String, content: String) |
348 |
352 |