equal
deleted
inserted
replaced
40 |
40 |
41 def session_dir(session: String): Path = |
41 def session_dir(session: String): Path = |
42 root_dir + Path.explode(sessions_structure(session).chapter_session) |
42 root_dir + Path.explode(sessions_structure(session).chapter_session) |
43 |
43 |
44 def theory_html(theory: Document_Info.Theory): Path = |
44 def theory_html(theory: Document_Info.Theory): Path = |
45 Path.explode(theory.print_short).html |
45 { |
|
46 val name1 = theory.print_short |
|
47 val name2 = if (Word.lowercase(name1) == "index") theory.name else name1 |
|
48 Path.explode(name2).html |
|
49 } |
46 |
50 |
47 def file_html(file: String): Path = |
51 def file_html(file: String): Path = |
48 Path.explode(file).squash.html |
52 Path.explode(file).squash.html |
49 |
53 |
50 def smart_html(theory: Document_Info.Theory, file: String): Path = |
54 def smart_html(theory: Document_Info.Theory, file: String): Path = |