equal
deleted
inserted
replaced
50 |
50 |
51 private val Section_Entry = new Regex("""^(\S.*)\s*$""") |
51 private val Section_Entry = new Regex("""^(\S.*)\s*$""") |
52 private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""") |
52 private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""") |
53 |
53 |
54 private def release_notes(): List[Entry] = |
54 private def release_notes(): List[Entry] = |
55 Section("Release notes", true) :: |
55 Section("Release Notes", true) :: |
56 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_)) |
56 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_)) |
57 |
57 |
58 private def examples(): List[Entry] = |
58 private def examples(): List[Entry] = |
59 Section("Examples", true) :: |
59 Section("Examples", true) :: |
60 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => |
60 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => |