1/* Title: Pure/Tools/doc.scala 2 Author: Makarius 3 4Access to Isabelle documentation. 5*/ 6 7package isabelle 8 9 10import scala.util.matching.Regex 11 12 13object Doc 14{ 15 /* dirs */ 16 17 def dirs(): List[Path] = 18 Path.split(Isabelle_System.getenv("ISABELLE_DOCS")) 19 20 21 /* contents */ 22 23 private def contents_lines(): List[(Path, String)] = 24 for { 25 dir <- dirs() 26 catalog = dir + Path.basic("Contents") 27 if catalog.is_file 28 line <- split_lines(Library.trim_line(File.read(catalog))) 29 } yield (dir, line) 30 31 sealed abstract class Entry 32 case class Section(text: String, important: Boolean) extends Entry 33 case class Doc(name: String, title: String, path: Path) extends Entry 34 case class Text_File(name: String, path: Path) extends Entry 35 36 def text_file(name: Path): Option[Text_File] = 37 { 38 val path = Path.variable("ISABELLE_HOME") + name 39 if (path.is_file) Some(Text_File(name.implode, path)) 40 else None 41 } 42 43 private val Section_Entry = new Regex("""^(\S.*)\s*$""") 44 private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""") 45 46 private def release_notes(): List[Entry] = 47 Section("Release notes", true) :: 48 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_)) 49 50 private def examples(): List[Entry] = 51 Section("Examples", true) :: 52 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => 53 text_file(file) match { 54 case Some(entry) => entry 55 case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file) 56 }) 57 58 def contents(): List[Entry] = 59 { 60 val main_contents = 61 for { 62 (dir, line) <- contents_lines() 63 entry <- 64 line match { 65 case Section_Entry(text) => 66 Library.try_unsuffix("!", text) match { 67 case None => Some(Section(text, false)) 68 case Some(txt) => Some(Section(txt, true)) 69 } 70 case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name))) 71 case _ => None 72 } 73 } yield entry 74 75 examples() ::: release_notes() ::: main_contents 76 } 77 78 def doc_names(): List[String] = 79 for (Doc(name, _, _) <- contents()) yield name 80 81 82 /* view */ 83 84 def view(path: Path) 85 { 86 if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true) 87 else { 88 val pdf = path.ext("pdf") 89 if (pdf.is_file) Isabelle_System.pdf_viewer(pdf) 90 else error("Bad Isabelle documentation file: " + pdf) 91 } 92 } 93 94 95 /* Isabelle tool wrapper */ 96 97 val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args => 98 { 99 val getopts = Getopts(""" 100Usage: isabelle doc [DOC ...] 101 102 View Isabelle documentation. 103""") 104 val docs = getopts(args) 105 106 val entries = contents() 107 if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true) 108 else { 109 docs.foreach(doc => 110 entries.collectFirst { case Doc(name, _, path) if doc == name => path } match { 111 case Some(path) => view(path) 112 case None => error("No Isabelle documentation entry: " + quote(doc)) 113 } 114 ) 115 } 116 }) 117} 118