# HG changeset patch # User wenzelm # Date 1645456991 -3600 # Node ID c212435866d6d65c038a3931578dcbbd4bbf548e # Parent 1fd78367c96f77f8b273a0fa6dd965b2e421909c clarified signature: more explicit section structure; diff -r 1fd78367c96f -r c212435866d6 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Mon Feb 21 15:33:04 2022 +0100 +++ b/src/Pure/Tools/doc.scala Mon Feb 21 16:23:11 2022 +0100 @@ -7,6 +7,9 @@ package isabelle +import scala.collection.mutable + + object Doc { /* dirs */ @@ -25,8 +28,8 @@ line <- Library.trim_split_lines(File.read(catalog)) } yield (dir, line) + case class Section(title: String, important: Boolean, entries: List[Entry]) sealed abstract class Entry - case class Heading(title: String, important: Boolean) extends Entry case class Doc(name: String, title: String, path: Path) extends Entry case class Text_File(name: String, path: Path) extends Entry @@ -38,47 +41,71 @@ } else None - private val Section_Entry = """^(\S.*)\s*$""".r - private val Doc_Entry = """^\s+(\S+)\s+(.+)\s*$""".r + def release_notes(): Section = + Section("Release Notes", true, + Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file)) - private def release_notes(): List[Entry] = - Heading("Release Notes", true) :: - Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file) - - private def examples(): List[Entry] = - Heading("Examples", true) :: + def examples(): Section = + Section("Examples", true, Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => text_file(file) match { case Some(entry) => entry case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file) - }) + })) + + def main_contents(): List[Section] = + { + val result = new mutable.ListBuffer[Section] + val entries = new mutable.ListBuffer[Entry] + var section: Option[Section] = None + + def flush(): Unit = + if (section.nonEmpty) { + result += section.get.copy(entries = entries.toList) + entries.clear() + section = None + } + + def begin(s: Section): Unit = + { + flush() + section = Some(s) + } + + val Section_ = """^(\S.*)\s*$""".r + val Doc_ = """^\s+(\S+)\s+(.+)\s*$""".r - def main_contents(): List[Entry] = - for { - (dir, line) <- contents_lines() - entry <- - line match { - case Section_Entry(text) => - Library.try_unsuffix("!", text) match { - case None => Some(Heading(text, false)) - case Some(txt) => Some(Heading(txt, true)) - } - case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name))) - case _ => None - } - } yield entry + for ((dir, line) <- contents_lines()) { + line match { + case Section_(text) => + Library.try_unsuffix("!", text) match { + case None => begin(Section(text, false, Nil)) + case Some(txt) => begin(Section(txt, true, Nil)) + } + case Doc_(name, title) => + entries += Doc(name, title, dir + Path.basic(name)) + case _ => + } + } - def contents(): List[Entry] = + flush() + result.toList + } + + def contents(): List[Section] = { - examples() ::: release_notes() ::: main_contents() + examples() :: release_notes() :: main_contents() } + def doc_entries(sections: List[Section]): List[Doc] = + sections.flatMap(_.entries).collect({ case doc: Doc => doc }) + object Doc_Names extends Scala.Fun_String("doc_names") { val here = Scala_Project.here def apply(arg: String): String = if (arg.nonEmpty) error("Bad argument: " + quote(arg)) - else cat_lines((for (Doc(name, _, _) <- contents()) yield name).sorted) + else cat_lines((for (doc <- doc_entries(contents())) yield doc.name).sorted) } @@ -107,13 +134,13 @@ """) val docs = getopts(args) - val entries = contents() + val sections = contents() if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true) else { - docs.foreach(doc => - entries.collectFirst { case Doc(name, _, path) if doc == name => path } match { - case Some(path) => view(path) - case None => error("No Isabelle documentation entry: " + quote(doc)) + docs.foreach(name => + doc_entries(sections).find(_.name == name) match { + case Some(doc) => view(doc.path) + case None => error("No Isabelle documentation entry: " + quote(name)) } ) } diff -r 1fd78367c96f -r c212435866d6 src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Mon Feb 21 15:33:04 2022 +0100 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Mon Feb 21 16:23:11 2022 +0100 @@ -19,7 +19,7 @@ class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) { - private val docs = Doc.contents() + private val sections = Doc.contents() private case class Documentation(name: String, title: String, path: Path) { @@ -33,15 +33,17 @@ } private val root = new DefaultMutableTreeNode - docs foreach { - case Doc.Heading(text, _) => - root.add(new DefaultMutableTreeNode(text)) - case Doc.Doc(name, title, path) => - root.getLastChild.asInstanceOf[DefaultMutableTreeNode] - .add(new DefaultMutableTreeNode(Documentation(name, title, path))) - case Doc.Text_File(name: String, path: Path) => - root.getLastChild.asInstanceOf[DefaultMutableTreeNode] - .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) + for (section <- sections) { + root.add(new DefaultMutableTreeNode(section.title)) + section.entries.foreach( + { + case Doc.Doc(name, title, path) => + root.getLastChild.asInstanceOf[DefaultMutableTreeNode] + .add(new DefaultMutableTreeNode(Documentation(name, title, path))) + case Doc.Text_File(name: String, path: Path) => + root.getLastChild.asInstanceOf[DefaultMutableTreeNode] + .add(new DefaultMutableTreeNode(Text_File(name, path.expand))) + }) } private val tree = new JTree(root) @@ -93,14 +95,15 @@ { var expand = true var visible = 0 - def make_visible(row: Int): Unit = { visible += 1; tree.expandRow(row) } - for ((entry, row) <- docs.zipWithIndex) { - entry match { - case Doc.Heading(_, important) => - expand = important - make_visible(row) - case _ => - if (expand) make_visible(row) + var row = 0 + def make_visible(): Unit = { visible += 1; tree.expandRow(row) } + for (section <- sections) { + expand = section.important + make_visible() + row += 1 + for (_ <- section.entries) { + if (expand) make_visible() + row += 1 } } tree.setRootVisible(false) diff -r 1fd78367c96f -r c212435866d6 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Feb 21 15:33:04 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Feb 21 16:23:11 2022 +0100 @@ -198,7 +198,7 @@ /* hyperlinks */ def hyperlink_doc(name: String): Option[Hyperlink] = - Doc.contents().collectFirst({ + Doc.contents().iterator.flatMap(_.entries.iterator).collectFirst({ case doc: Doc.Text_File if doc.name == name => doc.path case doc: Doc.Doc if doc.name == name => doc.path}).map(path => new Hyperlink {