--- 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 \<open>cartouche\<close> syntax instead.
+* Session ROOT files support 'chapter_definition', in order to associate
+a description for presentation purposes.
+
*** Isabelle/VSCode Prover IDE ***
--- /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."
--- 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 @@
<li style="list-style: none">
<ul>
- <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
+ <li><a href="ZF/index.html">ZF (Set Theory)</a>
+ offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
+ </li>
+
+ <li><a href="FOL/FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
provides basic classical and intuitionistic first-order logic. It is
polymorphic.
</li>
- <li><a href="ZF/index.html">ZF (Set Theory)</a>
- offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
- </li>
+ <li><a href="FOL/CCL/index.html">CCL (Classical Computational Logic)</a></li>
- <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
+ <li><a href="FOL/LCF/index.html">LCF (Logic of Computable Functions)</a></li>
- <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
-
- <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
+ <li><a href="FOL/FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
</ul>
</li>
</ul>
@@ -39,12 +39,12 @@
<li style="list-style: none">
<ul>
- <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
+ <li><a href="Misc/Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
- <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
+ <li><a href="Misc/CTT/index.html">CTT (Constructive Type Theory)</a>
is an extensional version of Martin-Löf's Type Theory.</li>
- <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+ <li><a href="Misc/Cube/index.html">Cube (The Lambda Cube)</a></li>
<li><a href="Pure/index.html">The Pure logical framework</a></li>
--- 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 "
--- 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 "
--- 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 "
--- 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>\<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/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 "
--- 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 "
--- 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);
--- 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) :::
--- 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;
--- 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)
--- 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 *)
--- 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)
--- 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";
-
--- 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 \<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/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 +
-"""
-<head>
- """ + HTML.head_meta + """
- <title>""" + title + """</title>
-</head>
-<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
- <center>
- <table width="100%" border="0" cellspacing="10" cellpadding="0">
- <tr>
- <td width="20%" valign="middle" align="center"><a href="https://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
+ 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)
+ }
- <td width="80%" valign="middle" align="center">
- <table width="90%" border="0" cellspacing="0" cellpadding="20">
- <tr>
- <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">""" + title + """</font></td>
- </tr>
- </table>
- </td>
- </tr>
- </table>
- </center>
- <hr />
-""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
-"""
-</body>
-""" + 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()
--- 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 ".") --
--- 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 =
--- 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 "
--- 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
--- 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))
}
--- 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
}
--- 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)
})
--- 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)