--- a/NEWS Fri Aug 26 21:25:35 2022 +0200
+++ b/NEWS Fri Aug 26 21:28:26 2022 +0200
@@ -12,6 +12,9 @@
* Old-style {* verbatim *} tokens have been discontinued (legacy feature
since Isabelle2019). INCOMPATIBILITY, use \<open>cartouche\<close> syntax instead.
+* Session ROOT files support 'chapter_definition', in order to associate
+a description for presentation purposes.
+
*** Isabelle/VSCode Prover IDE ***
--- a/src/Doc/System/Sessions.thy Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Doc/System/Sessions.thy Fri Aug 26 21:28:26 2022 +0200
@@ -38,18 +38,22 @@
The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
forms like identifiers, names, quoted strings, verbatim text, nested
- comments etc. The grammar for @{syntax session_chapter} and @{syntax
- session_entry} is given as syntax diagram below; each ROOT file may contain
- multiple specifications like this. Chapters help to organize browser info
- (\secref{sec:info}), but have no formal meaning. The default chapter is
- ``\<open>Unsorted\<close>''.
+ comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry}
+ and @{syntax session_entry} is given as syntax diagram below. Each ROOT file
+ may contain multiple specifications like this. Chapters help to organize
+ browser info (\secref{sec:info}), but have no formal meaning. The default
+ chapter is ``\<open>Unsorted\<close>''. Chapter definitions are optional: the main
+ purpose is to associate a description for presentation.
Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
\<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
file of that name.
\<^rail>\<open>
- @{syntax_def session_chapter}: @'chapter' @{syntax name}
+ @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} description
+ ;
+
+ @{syntax_def chapter_entry}: @'chapter' @{syntax name}
;
@{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
--- a/src/Pure/Isar/parse.ML Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Pure/Isar/parse.ML Fri Aug 26 21:28:26 2022 +0200
@@ -72,6 +72,7 @@
val path_input: Input.source parser
val path: string parser
val path_binding: (string * Position.T) parser
+ val chapter_name: (string * Position.T) parser
val session_name: (string * Position.T) parser
val theory_name: (string * Position.T) parser
val liberal_name: string parser
@@ -289,6 +290,7 @@
val path = path_input >> Input.string_of;
val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
+val chapter_name = group (fn () => "chapter name") name_position;
val session_name = group (fn () => "session name") name_position;
val theory_name = group (fn () => "theory name") name_position;
--- a/src/Pure/Sessions.thy Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Pure/Sessions.thy Fri Aug 26 21:28:26 2022 +0200
@@ -6,15 +6,18 @@
theory Sessions
imports Pure
- keywords "session" :: thy_decl
+ keywords "chapter_definition" "session" :: thy_decl
and "description" "directories" "options" "sessions" "theories"
"document_theories" "document_files" "export_files" :: quasi_command
and "global"
begin
ML \<open>
+ Outer_Syntax.command \<^command_keyword>\<open>chapter_definition\<close> "PIDE markup for session ROOT"
+ Sessions.chapter_definition_parser;
+
Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"
- Sessions.command_parser;
+ Sessions.session_parser;
\<close>
end
--- a/src/Pure/Thy/sessions.ML Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Pure/Thy/sessions.ML Fri Aug 26 21:28:26 2022 +0200
@@ -8,7 +8,8 @@
sig
val root_name: string
val theory_name: string
- val command_parser: (Toplevel.transition -> Toplevel.transition) parser
+ val chapter_definition_parser: (Toplevel.transition -> Toplevel.transition) parser
+ val session_parser: (Toplevel.transition -> Toplevel.transition) parser
end;
structure Sessions: SESSIONS =
@@ -49,7 +50,19 @@
in
-val command_parser =
+val chapter_definition_parser =
+ Parse.chapter_name --
+ (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) >> (fn (_, descr) =>
+ Toplevel.keep (fn state =>
+ let
+ val ctxt = Toplevel.context_of state;
+ val _ =
+ Context_Position.report ctxt
+ (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
+ Markup.comment;
+ in () end));
+
+val session_parser =
Parse.session_name --
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
--- a/src/Pure/Thy/sessions.scala Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Aug 26 21:28:26 2022 +0200
@@ -641,9 +641,9 @@
}
object Structure {
- val empty: Structure = make(Nil)
+ val empty: Structure = make(Chapter_Defs.empty, Nil)
- def make(infos: List[Info]): Structure = {
+ def make(chapter_defs: Chapter_Defs, infos: List[Info]): Structure = {
def add_edges(
graph: Graph[String, Info],
kind: String,
@@ -716,12 +716,13 @@
}
}
- new Structure(
- session_positions, session_directories, global_theories, build_graph, imports_graph)
+ new Structure(chapter_defs, session_positions, session_directories,
+ global_theories, build_graph, imports_graph)
}
}
final class Structure private[Sessions](
+ val chapter_defs: Chapter_Defs,
val session_positions: List[(String, Position.T)],
val session_directories: Map[JFile, String],
val global_theories: Map[String, String],
@@ -799,8 +800,7 @@
graph.restrict(graph.all_preds(sessions).toSet)
}
- new Structure(
- session_positions, session_directories, global_theories,
+ new Structure(chapter_defs, session_positions, session_directories, global_theories,
restrict(build_graph), restrict(imports_graph))
}
@@ -853,6 +853,7 @@
/* parser */
+ private val CHAPTER_DEFINITION = "chapter_definition"
private val CHAPTER = "chapter"
private val SESSION = "session"
private val IN = "in"
@@ -870,6 +871,7 @@
val root_syntax: Outer_Syntax =
Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
GLOBAL + IN +
+ (CHAPTER_DEFINITION, Keyword.THY_DECL) +
(CHAPTER, Keyword.THY_DECL) +
(SESSION, Keyword.THY_DECL) +
(DESCRIPTION, Keyword.QUASI_COMMAND) +
@@ -883,6 +885,7 @@
(EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
abstract class Entry
+ sealed case class Chapter_Def(pos: Position.T, name: String, description: String) extends Entry
sealed case class Chapter_Entry(name: String) extends Entry
sealed case class Session_Entry(
pos: Position.T,
@@ -906,12 +909,48 @@
document_theories.map(_._1)
}
+ object Chapter_Defs {
+ val empty: Chapter_Defs = new Chapter_Defs(Nil)
+ }
+
+ class Chapter_Defs private(rev_list: List[Chapter_Def]) {
+ def list: List[Chapter_Def] = rev_list.reverse
+
+ override def toString: String =
+ list.map(_.name).mkString("Chapter_Defs(", ", ", ")")
+
+ private def find(chapter: String): Option[Chapter_Def] =
+ rev_list.find(_.name == chapter)
+
+ def apply(chapter: String): String =
+ find(chapter) match {
+ case None => ""
+ case Some(ch_def) => ch_def.description
+ }
+
+ def + (ch_def: Chapter_Def): Chapter_Defs =
+ if (ch_def.description.isEmpty) this
+ else {
+ find(ch_def.name) match {
+ case None => new Chapter_Defs(ch_def :: rev_list)
+ case Some(old_def) =>
+ error("Duplicate chapter definition " + quote(ch_def.name) +
+ Position.here(old_def.pos) + Position.here(ch_def.pos))
+ }
+ }
+ }
+
private object Parsers extends Options.Parsers {
- private val chapter: Parser[Chapter_Entry] = {
- val chapter_name = atom("chapter name", _.is_name)
+ private val chapter_name: Parser[String] =
+ atom("chapter name", _.is_name)
+ private val chapter_def: Parser[Chapter_Def] =
+ command(CHAPTER_DEFINITION) ~!
+ (position(chapter_name) ~ $$$(DESCRIPTION) ~ text) ^^
+ { case _ ~ ((a, pos) ~ _ ~ b) => Chapter_Def(pos, a, b) }
+
+ private val chapter_entry: Parser[Chapter_Entry] =
command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
- }
private val session_entry: Parser[Session_Entry] = {
val option =
@@ -968,8 +1007,8 @@
def parse_root(path: Path): List[Entry] = {
val toks = Token.explode(root_syntax.keywords, File.read(path))
val start = Token.Pos.file(path.implode)
-
- parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
+ val parser: Parser[Entry] = chapter_def | chapter_entry | session_entry
+ parse_all(rep(parser), Token.reader(toks, start)) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
@@ -982,15 +1021,22 @@
for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
yield entry.asInstanceOf[Session_Entry]
- def read_root(options: Options, select: Boolean, path: Path): List[Info] = {
+ def read_root(
+ options: Options,
+ select: Boolean,
+ path: Path,
+ chapter_defs: Chapter_Defs
+ ): (List[Info], Chapter_Defs) = {
+ var chapter_defs1 = chapter_defs
var entry_chapter = UNSORTED
val infos = new mutable.ListBuffer[Info]
parse_root(path).foreach {
- case Chapter_Entry(name) => entry_chapter = name
+ case ch_def: Chapter_Def => chapter_defs1 += ch_def
+ case entry: Chapter_Entry => entry_chapter = entry.name
case entry: Session_Entry =>
infos += make_info(options, select, path.dir, entry_chapter, entry)
}
- infos.toList
+ (infos.toList, chapter_defs1)
}
def parse_roots(roots: Path): List[String] = {
@@ -1063,7 +1109,18 @@
}
}.toList.map(_._2)
- Structure.make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
+ val (chapter_defs, info_roots) = {
+ var chapter_defs = Chapter_Defs.empty
+ val result = new mutable.ListBuffer[Info]
+ for { (select, path) <- unique_roots } {
+ val (infos, chapter_defs1) = read_root(options, select, path, chapter_defs)
+ chapter_defs = chapter_defs1
+ result ++= infos
+ }
+ (chapter_defs, result.toList)
+ }
+
+ Structure.make(chapter_defs, info_roots ::: infos)
}