isabelle: src/Pure/Tools/doc.scala@4829e4c68d7c (annotated)

52444 2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	1	/* Title: Pure/Tools/doc.scala
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	2	Author: Makarius
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	3
81353 4829e4c68d7c tuned description: plain text documentation is also supported; wenzelm parents: 81350 diff changeset	4	Access to Isabelle examples and documentation.
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	5	*/
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	6
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	7	package isabelle
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	8
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	9
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	10	import scala.collection.mutable
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	11
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	12
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	13	object Doc {
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	14	/* entries */
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	15
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	16	case class Section(title: String, important: Boolean, entries: List[Entry])
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	17	case class Entry(name: String, path: Path, title: String = "") {
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	18	def view(): Unit = Doc.view(path)
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	19	override def toString: String = // GUI label
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	20	if (title.nonEmpty) {
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	21	"<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	22	}
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	23	else name
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	24	}
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	25
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	26	def plain_file(path: Path): Option[Entry] =
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	27	if (path.is_file && !path.is_pdf) {
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	28	val a = path.implode
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	29	val b = Library.try_unprefix("$ISABELLE_HOME/", a).getOrElse(a)
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	30	Some(Entry(b, path))
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	31	}
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	32	else None
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	33
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	34
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	35	/* contents */
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	36
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	37	def dirs(): List[Path] =
67604 02cf352cbc4c permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc; wenzelm parents: 67471 diff changeset	38	Path.split(Isabelle_System.getenv("ISABELLE_DOCS"))
52740 bceec99254b0 documentation is always in PDF; wenzelm parents: 52542 diff changeset	39
56422 7490555d7dff clarified Doc entry: more explicit path; wenzelm parents: 56276 diff changeset	40	private def contents_lines(): List[(Path, String)] =
52444 2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	41	for {
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	42	dir <- dirs()
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	43	catalog = dir + Path.basic("Contents")
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	44	if catalog.is_file
73276 54065cbf7134 tuned; wenzelm parents: 72770 diff changeset	45	line <- Library.trim_split_lines(File.read(catalog))
56422 7490555d7dff clarified Doc entry: more explicit path; wenzelm parents: 56276 diff changeset	46	} yield (dir, line)
52444 2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	47
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	48	object Contents {
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	49	def apply(sections: List[Section]): Contents = new Contents(sections)
6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	50
6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	51	def section(title: String, important: Boolean, entries: List[Entry]): Contents =
6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	52	apply(List(Section(title, important, entries)))
6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	53	}
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	54	class Contents private(val sections: List[Section]) {
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	55	def ++ (other: Contents): Contents = new Contents(sections ::: other.sections)
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	56	def entries(name: String => Boolean = _ => true, pdf: Boolean = false): List[Entry] =
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	57	sections.flatMap(s => s.entries.filter(e => name(e.name) && (!pdf \|\| e.path.is_pdf)))
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	58	}
53777 06a6216f733e immediate access to some elementary examples; wenzelm parents: 52740 diff changeset	59
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	60	def release_notes(): Contents =
6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	61	Contents.section("Release Notes", true,
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	62	Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(plain_file))
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	63
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	64	def examples(): Contents =
6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	65	Contents.section("Examples", true,
56424 7032378cc097 proper settings instead of hard-wired information; wenzelm parents: 56423 diff changeset	66	Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	67	plain_file(file) match {
56424 7032378cc097 proper settings instead of hard-wired information; wenzelm parents: 56423 diff changeset	68	case Some(entry) => entry
56425 d12653fbd5b1 tuned error; wenzelm parents: 56424 diff changeset	69	case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	70	}))
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	71
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	72	def main_contents(): Contents = {
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	73	val result = new mutable.ListBuffer[Section]
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	74	val entries = new mutable.ListBuffer[Entry]
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	75	var section: Option[Section] = None
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	76
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	77	def flush(): Unit =
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	78	if (section.nonEmpty) {
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	79	result += section.get.copy(entries = entries.toList)
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	80	entries.clear()
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	81	section = None
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	82	}
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	83
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	84	def begin(s: Section): Unit = {
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	85	flush()
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	86	section = Some(s)
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	87	}
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	88
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	89	val Section_ = """^(\S.)\s$""".r
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	90	val Entry_ = """^\s+(\S+)\s+(.+)\s*$""".r
53777 06a6216f733e immediate access to some elementary examples; wenzelm parents: 52740 diff changeset	91
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	92	for ((dir, line) <- contents_lines()) {
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	93	line match {
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	94	case Section_(text) =>
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	95	Library.try_unsuffix("!", text) match {
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	96	case None => begin(Section(text, false, Nil))
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	97	case Some(txt) => begin(Section(txt, true, Nil))
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	98	}
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	99	case Entry_(name, title) =>
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	100	val path = dir + Path.basic(name)
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	101	entries += Entry(name, if (path.is_file) path else path.pdf, title = title)
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	102	case _ =>
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	103	}
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	104	}
75114 1fd78367c96f clarified signature; wenzelm parents: 73565 diff changeset	105
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	106	flush()
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	107	Contents(result.toList)
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	108	}
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	109
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	110	def contents(): Contents = {
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75116 diff changeset	111	examples() ++ release_notes() ++ main_contents()
61157 13f4056c42d7 clarified order; wenzelm parents: 56831 diff changeset	112	}
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	113
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	114	object Doc_Names extends Scala.Fun_String("doc_names") {
72760 042180540068 clarified protocol: Doc.check at run-time via Scala function; wenzelm parents: 71601 diff changeset	115	val here = Scala_Project.here
042180540068 clarified protocol: Doc.check at run-time via Scala function; wenzelm parents: 71601 diff changeset	116	def apply(arg: String): String =
042180540068 clarified protocol: Doc.check at run-time via Scala function; wenzelm parents: 71601 diff changeset	117	if (arg.nonEmpty) error("Bad argument: " + quote(arg))
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	118	else cat_lines((for (entry <- contents().entries(pdf = true)) yield entry.name).sorted)
72760 042180540068 clarified protocol: Doc.check at run-time via Scala function; wenzelm parents: 71601 diff changeset	119	}
67471 bddfa23a4ea9 formal treatment of documentation names; wenzelm parents: 67178 diff changeset	120
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	121
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	122	/* view */
9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	123
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	124	def view(path: Path): Unit = {
75120 488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	125	if (!path.is_file) error("Bad Isabelle documentation file: " + path)
488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	126	else if (path.is_pdf) Isabelle_System.pdf_viewer(path)
488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	127	else Output.writeln(Library.trim_line(File.read(path)), stdout = true)
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	128	}
52444 2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	129
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	130
62831 5560905a32ae prefer internal tool; wenzelm parents: 62454 diff changeset	131	/* Isabelle tool wrapper */
52444 2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala; wenzelm parents: 52429 diff changeset	132
81353 4829e4c68d7c tuned description: plain text documentation is also supported; wenzelm parents: 81350 diff changeset	133	val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation",
75394 42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	134	Scala_Project.here,
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	135	{ args =>
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	136	val getopts = Getopts("""
62438 42e13a4f52f5 moved getopts to Scala; wenzelm parents: 61157 diff changeset	137	Usage: isabelle doc [DOC ...]
42e13a4f52f5 moved getopts to Scala; wenzelm parents: 61157 diff changeset	138
81353 4829e4c68d7c tuned description: plain text documentation is also supported; wenzelm parents: 81350 diff changeset	139	View Isabelle documentation.
62438 42e13a4f52f5 moved getopts to Scala; wenzelm parents: 61157 diff changeset	140	""")
75394 42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	141	val docs = getopts(args)
62438 42e13a4f52f5 moved getopts to Scala; wenzelm parents: 61157 diff changeset	142
75394 42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	143	if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	144	else {
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	145	docs.foreach(name =>
81350 1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	146	contents().entries(name = docs.contains).headOption match {
1818358373e2 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; wenzelm parents: 75394 diff changeset	147	case Some(entry) => entry.view()
75394 42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	148	case None => error("No Isabelle documentation entry: " + quote(name))
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	149	}
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	150	)
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	151	}
42267c650205 tuned formatting; wenzelm parents: 75393 diff changeset	152	})
52427 9d1cc9a22177 Scala version of "isabelle doc"; wenzelm parents: diff changeset	153	}

author	wenzelm
	Tue, 05 Nov 2024 23:45:39 +0100
changeset 81353	4829e4c68d7c
parent 81350	1818358373e2
child 81656	7593c0976dc6
permissions	-rw-r--r--