# HG changeset patch # User wenzelm # Date 1661548627 -7200 # Node ID 8f1bb89ddf4bfc974048a0aabc9d9aaee918a0f3 # Parent c8d9fbe2dedd6ea608ec541de4b481af11d3e975# Parent 1f6d79b6222296093b705ed7500b1d954d72bc70 merged diff -r c8d9fbe2dedd -r 8f1bb89ddf4b NEWS --- a/NEWS Fri Aug 26 12:43:07 2022 +0100 +++ b/NEWS Fri Aug 26 23:17:07 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 c8d9fbe2dedd -r 8f1bb89ddf4b ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -0,0 +1,35 @@ +chapter_definition HOL + description " + Higher-Order Logic. + + Isabelle/HOL is a version of classical higher-order logic resembling + that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL). + " + +chapter_definition ZF + description " + Zermelo-Fraenkel set theory. + + Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top of + Isabelle/FOL. + " + +chapter_definition FOL + description " + First-Order Logic with some variations: single-sorted vs. many-sorted + (polymorphic), classical vs. intuitionistic, domain-theory (LCF). + " + +chapter_definition Pure + description " + The Pure logical framework. + + Isabelle/Pure is a version of intuitionistic higher-order logic that + expresses rules for Natural Deduction declaratively. + " + +chapter_definition Misc + description "Miscellaneous object-logics, tools, and experiments." + +chapter_definition Doc + description "Sources of Documentation." diff -r c8d9fbe2dedd -r 8f1bb89ddf4b lib/html/library_index_content.template --- a/lib/html/library_index_content.template Fri Aug 26 12:43:07 2022 +0100 +++ b/lib/html/library_index_content.template Fri Aug 26 23:17:07 2022 +0200 @@ -16,20 +16,20 @@
    • @@ -39,12 +39,12 @@
    • -
    • Sequents (first-order, modal and linear logics)
      • +
    • Sequents (first-order, modal and linear logics)
      • -
    • CTT (Constructive Type Theory) +
    • CTT (Constructive Type Theory) is an extensional version of Martin-Löf's Type Theory.
      • -
    • Cube (The Lambda Cube)
      • +
    • Cube (The Lambda Cube)
    • The Pure logical framework
      • diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/CCL/ROOT --- a/src/CCL/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/CCL/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter CCL +chapter FOL session CCL = Pure + description " diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/CTT/ROOT --- a/src/CTT/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/CTT/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter CTT +chapter Misc session CTT = Pure + description " diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Cube/ROOT --- a/src/Cube/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Cube/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter Cube +chapter Misc session Cube = Pure + description " diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Doc/System/Sessions.thy Fri Aug 26 23:17:07 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 c8d9fbe2dedd -r 8f1bb89ddf4b src/FOLP/ROOT --- a/src/FOLP/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/FOLP/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter FOLP +chapter FOL session FOLP = Pure + description " diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/LCF/ROOT --- a/src/LCF/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/LCF/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter LCF +chapter FOL session LCF = Pure + description " diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/General/name_space.ML Fri Aug 26 23:17:07 2022 +0200 @@ -114,8 +114,7 @@ serial: serial}; fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) = - Position.make_entity_markup def serial kind (name, pos) - ||> not (#def def orelse theory_long_name = "") ? cons (Markup.def_theoryN, theory_long_name); + Position.make_entity_markup def serial kind (name, pos); fun print_entry_ref kind (name, entry) = quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name); diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/General/position.scala --- a/src/Pure/General/position.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/General/position.scala Fri Aug 26 23:17:07 2022 +0200 @@ -25,8 +25,6 @@ val Def_File = new Properties.String(Markup.DEF_FILE) val Def_Id = new Properties.Long(Markup.DEF_ID) - val Def_Theory = new Properties.String(Markup.DEF_THEORY) - object Line_File { def apply(line: Int, file: String): T = (if (line > 0) Line(line) else Nil) ::: diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/Isar/parse.ML Fri Aug 26 23:17:07 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 c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/Isar/parse.scala Fri Aug 26 23:17:07 2022 +0200 @@ -71,6 +71,7 @@ def path: Parser[String] = atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content)) + def chapter_name: Parser[String] = atom("chapter name", _.is_system_name) def session_name: Parser[String] = atom("session name", _.is_system_name) def theory_name: Parser[String] = atom("theory name", _.is_system_name) diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/PIDE/markup.ML Fri Aug 26 23:17:07 2022 +0200 @@ -64,7 +64,6 @@ val position_properties: string list val position_property: Properties.entry -> bool val def_name: string -> string - val def_theoryN: string val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T @@ -427,8 +426,6 @@ SOME b => b | NONE => make_def a); -val def_theoryN = "def_theory"; - (* expression *) diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/PIDE/markup.scala Fri Aug 26 23:17:07 2022 +0200 @@ -146,8 +146,6 @@ val DEF_FILE = "def_file" val DEF_ID = "def_id" - val DEF_THEORY = "def_theory" - val POSITION = "position" val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/ROOT.ML Fri Aug 26 23:17:07 2022 +0200 @@ -364,4 +364,3 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML"; - diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/Sessions.thy --- a/src/Pure/Sessions.thy Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/Sessions.thy Fri Aug 26 23:17:07 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 c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/Thy/browser_info.scala --- a/src/Pure/Thy/browser_info.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/Thy/browser_info.scala Fri Aug 26 23:17:07 2022 +0200 @@ -57,6 +57,12 @@ dir } + def clean_directory(dir: Path): Path = { + check_directory(dir) + Isabelle_System.rm_tree(dir) // guarded by check_directory! + Isabelle_System.new_directory(dir + PATH) + } + /* content */ @@ -129,8 +135,14 @@ } sealed case class Index(kind: String, items: List[Item]) { - def +(item: Item): Index = - Index(kind, (item :: items.filterNot(_.name == item.name)).sortBy(_.name)) + def is_empty: Boolean = items.isEmpty + + def ++ (more_items: List[Item]): Index = { + val items1 = items.filterNot(item => more_items.exists(_.name == item.name)) + val items2 = (more_items ::: items1).sortBy(_.name) + Index(kind, items2) + } + def + (item: Item): Index = this ++ List(item) def json: JSON.T = JSON.Object("kind" -> kind, "items" -> items.map(_.json)) def print_json: JSON.S = JSON.Format.pretty_print(json) @@ -145,16 +157,16 @@ entity: Markup.Elements = Markup.Elements.empty, language: Markup.Elements = Markup.Elements.empty) - val elements1: Elements = + val default_elements: Elements = Elements( html = Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE, entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT, Markup.CLASS, Markup.LOCALE, Markup.FREE)) - val elements2: Elements = + val extra_elements: Elements = Elements( - html = elements1.html ++ Rendering.markdown_elements, + html = default_elements.html ++ Rendering.markdown_elements, language = Markup.Elements(Markup.Language.DOCUMENT)) @@ -163,7 +175,7 @@ def context( sessions_structure: Sessions.Structure, - elements: Elements, + elements: Elements = default_elements, root_dir: Path = Path.current, document_info: Document_Info = Document_Info.empty ): Context = new Context(sessions_structure, elements, root_dir, document_info) @@ -182,11 +194,14 @@ def theory_by_file(session: String, file: String): Option[Document_Info.Theory] = document_info.theory_by_file(session, file) - def session_dir(session: String): Path = - root_dir + Path.explode(sessions_structure(session).chapter_session) + def session_chapter(session: String): String = + sessions_structure(session).chapter - def chapter_dir(chapter: String): Path = - root_dir + Path.basic(chapter) + def chapter_dir(session: String): Path = + root_dir + Path.basic(session_chapter(session)) + + def session_dir(session: String): Path = + chapter_dir(session) + Path.basic(session) def theory_dir(theory: Document_Info.Theory): Path = session_dir(theory.dynamic_session) @@ -194,7 +209,7 @@ def theory_html(theory: Document_Info.Theory): Path = { def check(name: String): Option[Path] = { - val path = Path.explode(name).html + val path = Path.basic(name).html if (Path.eq_case_insensitive(path, Path.index_html)) None else Some(path) } @@ -269,31 +284,26 @@ /* maintain presentation structure */ - def update_chapter( - chapter: String, - session_name: String, - session_description: String - ): Unit = synchronized { - val dir = Meta_Data.init_directory(chapter_dir(chapter)) + def update_chapter(session_name: String, session_description: String): Unit = synchronized { + val dir = Meta_Data.init_directory(chapter_dir(session_name)) Meta_Data.change(dir, Meta_Data.INDEX) { text => val index0 = Meta_Data.Index.parse(text, "chapter") val item = Meta_Data.Item(session_name, description = session_description) val index = index0 + item - val sessions = index.items if (index != index0) { - val title = "Isabelle/" + chapter + " sessions" + val title = "Isabelle/" + session_chapter(session_name) + " sessions" HTML.write_document(dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), HTML.chapter(title) :: - (if (sessions.isEmpty) Nil + (if (index.is_empty) Nil else List(HTML.div("sessions", List(HTML.description( - sessions.map(session => - (List(HTML.link(session.name + "/index.html", HTML.text(session.name))), - if (session.description.isEmpty) Nil - else HTML.break ::: List(HTML.pre(HTML.text(session.description)))))))))), + index.items.map(item => + (List(HTML.link(item.name + "/index.html", HTML.text(item.name))), + if (item.description.isEmpty) Nil + else HTML.break ::: List(HTML.pre(HTML.text(item.description)))))))))), root = Some(root_dir)) } @@ -306,36 +316,39 @@ HTML.init_fonts(root_dir) Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), root_dir + Path.explode("isabelle.gif")) - val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" - File.write(root_dir + Path.explode("index.html"), - HTML.header + -""" - - """ + HTML.head_meta + """ - """ + title + """ - - -
      - - - + Meta_Data.change(root_dir, Meta_Data.INDEX) { text => + val index0 = Meta_Data.Index.parse(text, "root") + val index = { + val items1 = + for (entry <- sessions_structure.chapter_defs.list) + yield Meta_Data.Item(entry.name, description = entry.description) + val items2 = + (for { + (name, _) <- sessions_structure.chapters.iterator + if !items1.exists(_.name == name) + } yield Meta_Data.Item(name)).toList + index0 ++ (items1 ::: items2) + } - - -
      [Isabelle] - - - - -
      """ + title + """
      -
      -
      -
      -""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) + -""" - -""" + HTML.footer) + if (index != index0) { + val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" + HTML.write_document(root_dir, "index.html", + List(HTML.title(title + Isabelle_System.isabelle_heading())), + HTML.chapter(title) :: + (if (index.is_empty) Nil + else + List(HTML.div("sessions", + List(HTML.description( + index.items.map(item => + (List(HTML.link(item.name + "/index.html", HTML.text(item.name))), + if (item.description.isEmpty) Nil + else HTML.break ::: List(HTML.pre(HTML.text(item.description)))))))))), + root = Some(root_dir)) + } + + index.print_json + } } } @@ -532,8 +545,8 @@ val session_dir = context.session_dir(session_name).expand progress.echo("Presenting " + session_name + " in " + session_dir + " ...") - Meta_Data.init_directory(context.chapter_dir(session_info.chapter)) - Meta_Data.init_directory(session_dir) + Meta_Data.init_directory(context.chapter_dir(session_name)) + Meta_Data.clean_directory(session_dir) val session = context.document_info.the_session(session_name) @@ -632,7 +645,7 @@ Meta_Data.set_build_uuid(session_dir, session.build_uuid) - context.update_chapter(session_info.chapter, session_name, session_info.description) + context.update_chapter(session_name, session_info.description) } def build( @@ -647,7 +660,7 @@ progress.echo("Presentation in " + root_dir) using(Export.open_database_context(store)) { database_context => - val context0 = context(deps.sessions_structure, elements1, root_dir = root_dir) + val context0 = context(deps.sessions_structure, root_dir = root_dir) val sessions1 = deps.sessions_structure.build_requirements(sessions).filter { session_name => @@ -662,7 +675,7 @@ } val context1 = - context(deps.sessions_structure, elements1, root_dir = root_dir, + context(deps.sessions_structure, root_dir = root_dir, document_info = Document_Info.read(database_context, deps, sessions1)) context1.update_root() diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/Thy/sessions.ML --- a/src/Pure/Thy/sessions.ML Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/Thy/sessions.ML Fri Aug 26 23:17:07 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 c8d9fbe2dedd -r 8f1bb89ddf4b src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Aug 26 23:17:07 2022 +0200 @@ -167,7 +167,7 @@ val groups = if (info.groups.isEmpty) "" else info.groups.mkString(" (", " ", ")") - progress.echo("Session " + info.chapter_session + groups) + progress.echo("Session " + info.chapter + "/" + session_name + groups) } val dependencies = resources.session_dependencies(info) @@ -477,8 +477,6 @@ export_classpath: List[String], meta_digest: SHA1.Digest ) { - def chapter_session: String = chapter + "/" + name - def deps: List[String] = parent.toList ::: imports def deps_base(session_bases: String => Base): Base = { @@ -643,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, @@ -718,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], @@ -801,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)) } @@ -855,6 +853,7 @@ /* parser */ + private val CHAPTER_DEFINITION = "chapter_definition" private val CHAPTER = "chapter" private val SESSION = "session" private val IN = "in" @@ -872,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) + @@ -885,7 +885,8 @@ (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND) abstract class Entry - sealed case class Chapter(name: String) extends 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, name: String, @@ -908,12 +909,45 @@ 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] = { - val chapter_name = 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) } - command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) } - } + 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 = @@ -970,8 +1004,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) } @@ -984,15 +1018,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(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] = { @@ -1065,7 +1106,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) } @@ -1199,7 +1251,7 @@ val augment_table: PostgreSQL.Source = "ALTER TABLE IF EXISTS " + table.ident + - " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql) + " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql) } def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store = diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Sequents/ROOT --- a/src/Sequents/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Sequents/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter Sequents +chapter Misc session Sequents = Pure + description " diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Tools/ROOT --- a/src/Tools/ROOT Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Tools/ROOT Fri Aug 26 23:17:07 2022 +0200 @@ -1,4 +1,4 @@ -chapter Tools +chapter Misc session Tools = Pure + theories diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Tools/VSCode/src/dynamic_output.scala --- a/src/Tools/VSCode/src/dynamic_output.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Tools/VSCode/src/dynamic_output.scala Fri Aug 26 23:17:07 2022 +0200 @@ -46,7 +46,7 @@ uri = File.uri(Path.explode(source).absolute_file) } yield HTML.link(uri.toString + "#" + def_line, body) } - val elements = Browser_Info.elements2.copy(entity = Markup.Elements.full) + val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full) val html = node_context.make_html(elements, Pretty.separate(st1.output)) channel.write(LSP.Dynamic_Output(HTML.source(html).toString)) } diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Tools/VSCode/src/preview_panel.scala Fri Aug 26 23:17:07 2022 +0200 @@ -28,9 +28,10 @@ val snapshot = model.snapshot() if (snapshot.is_outdated) m else { - val document = - Browser_Info.context(resources.sessions_structure, Browser_Info.elements2). - preview_document(snapshot) + val context = + Browser_Info.context(resources.sessions_structure, + elements = Browser_Info.extra_elements) + val document = context.preview_document(snapshot) channel.write(LSP.Preview_Response(file, column, document.title, document.content)) m - file } diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Tools/VSCode/src/state_panel.scala --- a/src/Tools/VSCode/src/state_panel.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Tools/VSCode/src/state_panel.scala Fri Aug 26 23:17:07 2022 +0200 @@ -69,7 +69,7 @@ uri = File.uri(Path.explode(source).absolute_file) } yield HTML.link(uri.toString + "#" + def_line, body) } - val elements = Browser_Info.elements2.copy(entity = Markup.Elements.full) + val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full) val html = node_context.make_html(elements, Pretty.separate(body)) output(HTML.source(html).toString) }) diff -r c8d9fbe2dedd -r 8f1bb89ddf4b src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Fri Aug 26 12:43:07 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Fri Aug 26 23:17:07 2022 +0200 @@ -313,9 +313,11 @@ } yield { val snapshot = model.await_stable_snapshot() + val context = + Browser_Info.context(PIDE.resources.sessions_structure, + elements = Browser_Info.extra_elements) val document = - Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2). - preview_document(snapshot, + context.preview_document(snapshot, plain_text = query.startsWith(plain_text_prefix), fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name))) HTTP.Response.html(document.content)