# HG changeset patch # User wenzelm # Date 1661542106 -7200 # Node ID 27d98da31985231150f64bdf649c32cef9ed3014 # Parent ce892601d775a28166253059e2ef303b307eb0c5 support 'chapter_definition' with description for presentation purposes; diff -r ce892601d775 -r 27d98da31985 NEWS --- 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 \cartouche\ syntax instead. +* Session ROOT files support 'chapter_definition', in order to associate +a description for presentation purposes. + *** Isabelle/VSCode Prover IDE *** diff -r ce892601d775 -r 27d98da31985 src/Doc/System/Sessions.thy --- 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>\outer syntax\ 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 - ``\Unsorted\''. + 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 ``\Unsorted\''. 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>\isabelle-root\ for session ROOT files, which is enabled by default for any file of that name. \<^rail>\ - @{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? '=' \ diff -r ce892601d775 -r 27d98da31985 src/Pure/Isar/parse.ML --- 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; diff -r ce892601d775 -r 27d98da31985 src/Pure/Sessions.thy --- 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 \ + Outer_Syntax.command \<^command_keyword>\chapter_definition\ "PIDE markup for session ROOT" + Sessions.chapter_definition_parser; + Outer_Syntax.command \<^command_keyword>\session\ "PIDE markup for session ROOT" - Sessions.command_parser; + Sessions.session_parser; \ end diff -r ce892601d775 -r 27d98da31985 src/Pure/Thy/sessions.ML --- 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 ".") -- diff -r ce892601d775 -r 27d98da31985 src/Pure/Thy/sessions.scala --- 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) }