equal
deleted
inserted
replaced
44 private val Section_Entry = new Regex("""^(\S.*)\s*$""") |
44 private val Section_Entry = new Regex("""^(\S.*)\s*$""") |
45 private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""") |
45 private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""") |
46 |
46 |
47 private def release_notes(): List[Entry] = |
47 private def release_notes(): List[Entry] = |
48 Section("Release Notes", true) :: |
48 Section("Release Notes", true) :: |
49 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_)) |
49 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file) |
50 |
50 |
51 private def examples(): List[Entry] = |
51 private def examples(): List[Entry] = |
52 Section("Examples", true) :: |
52 Section("Examples", true) :: |
53 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => |
53 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => |
54 text_file(file) match { |
54 text_file(file) match { |