equal
deleted
inserted
replaced
56 case Some(entry) => entry |
56 case Some(entry) => entry |
57 case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file) |
57 case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file) |
58 }) |
58 }) |
59 |
59 |
60 def contents(): List[Entry] = |
60 def contents(): List[Entry] = |
61 (for { |
61 { |
62 (dir, line) <- contents_lines() |
62 val main_contents = |
63 entry <- |
63 for { |
64 line match { |
64 (dir, line) <- contents_lines() |
65 case Section_Entry(text) => |
65 entry <- |
66 Library.try_unsuffix("!", text) match { |
66 line match { |
67 case None => Some(Section(text, false)) |
67 case Section_Entry(text) => |
68 case Some(txt) => Some(Section(txt, true)) |
68 Library.try_unsuffix("!", text) match { |
69 } |
69 case None => Some(Section(text, false)) |
70 case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name))) |
70 case Some(txt) => Some(Section(txt, true)) |
71 case _ => None |
71 } |
72 } |
72 case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name))) |
73 } yield entry) ::: release_notes() ::: examples() |
73 case _ => None |
|
74 } |
|
75 } yield entry |
|
76 |
|
77 examples() ::: release_notes() ::: main_contents |
|
78 } |
74 |
79 |
75 |
80 |
76 /* view */ |
81 /* view */ |
77 |
82 |
78 def view(path: Path) |
83 def view(path: Path) |
102 ) |
107 ) |
103 } |
108 } |
104 } |
109 } |
105 } |
110 } |
106 } |
111 } |
107 |
|