# HG changeset patch # User wenzelm # Date 1667249888 -3600 # Node ID d9c78a18b44b240b9f8811de8c216665556742df # Parent 8cb1413846826e2463129955b6dc992350000739# Parent d0a1f3eb09823d1650b3c1600d90a951c0f2b506 merged diff -r 8cb141384682 -r d9c78a18b44b Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Oct 28 06:34:26 2022 +0000 +++ b/Admin/components/components.sha1 Mon Oct 31 21:58:08 2022 +0100 @@ -90,6 +90,7 @@ 813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.tar.gz 6e63f9f354b8c06035952845b987080699a12d55 e-2.6-1.tar.gz a3bebab5df4294dac2dd7fd2065a94df00e0b3ff e-2.6.tar.gz +239e7b8bebbfc29a1c5151e8fb261ffad44877f1 easychair-3.5.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz @@ -104,6 +105,7 @@ 9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz 212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz 6d4dbb6f2bde5804298d9008e3edceb0b9ee20ae flatlaf-2.4.tar.gz +b1c40ce6c087da7e70e221ddd3fcadfa569acb2f foiltex-2.1.4b.tar.gz f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz 71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz @@ -279,6 +281,7 @@ 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz 759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz 1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz +5557b396f5a9aa22388d3e2171f9bc58e4bd6cd7 lipics-3.1.2.tar.gz 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz 400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz diff -r 8cb141384682 -r d9c78a18b44b Admin/components/main --- a/Admin/components/main Fri Oct 28 06:34:26 2022 +0000 +++ b/Admin/components/main Mon Oct 31 21:58:08 2022 +0100 @@ -6,7 +6,9 @@ csdp-6.1.1 cvc4-1.8 e-2.6-1 +easychair-3.5 flatlaf-2.4 +foiltex-2.1.4b idea-icons-20210508 isabelle_fonts-20211004 isabelle_setup-20221028 @@ -15,6 +17,7 @@ jfreechart-1.5.3 jortho-1.0-2 kodkodi-1.5.7 +lipics-3.1.2 minisat-2.2.1-1 mlton-20210117-1 nunchaku-0.5 diff -r 8cb141384682 -r d9c78a18b44b NEWS --- a/NEWS Fri Oct 28 06:34:26 2022 +0000 +++ b/NEWS Mon Oct 31 21:58:08 2022 +0100 @@ -7,6 +7,16 @@ New in this Isabelle version ---------------------------- +*** Document preparation *** + +* Various well-known LaTeX styles are included as Isabelle components, +with demo documents in the regular Isabelle "doc" space: + + - Easychair as session "Demo_Easychair" / doc "demo_easychair" + - FoilTeX as session "Demo_FoilTeX" / doc "demo_foiltex" + - Dagstuhl LIPIcs style as session "Demo_LIPIcs" / doc "demo_lipics" + + *** HOL *** * Theory "HOL.Fun": diff -r 8cb141384682 -r d9c78a18b44b doc/Contents --- a/doc/Contents Fri Oct 28 06:34:26 2022 +0000 +++ b/doc/Contents Mon Oct 31 21:58:08 2022 +0100 @@ -18,8 +18,14 @@ system The Isabelle System Manual jedit Isabelle/jEdit +Demo Documents + demo_easychair Demo for Easychair style + demo_foiltex Demo for FoilTeX: slides in LaTeX + demo_lipics Demo for Dagstuhl LIPIcs style + Old Isabelle Manuals tutorial Tutorial on Isabelle/HOL intro Old Introduction to Isabelle logics Isabelle's Logics: HOL and misc logics logics-ZF Isabelle's Logics: FOL and ZF + diff -r 8cb141384682 -r d9c78a18b44b etc/build.props --- a/etc/build.props Fri Oct 28 06:34:26 2022 +0000 +++ b/etc/build.props Mon Oct 31 21:58:08 2022 +0100 @@ -11,16 +11,19 @@ src/HOL/Tools/Mirabelle/mirabelle.scala \ src/HOL/Tools/Nitpick/kodkod.scala \ src/Pure/Admin/afp.scala \ + src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cvc5.scala \ - src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cygwin.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_e.scala \ + src/Pure/Admin/build_easychair.scala \ + src/Pure/Admin/build_foiltex.scala \ src/Pure/Admin/build_fonts.scala \ src/Pure/Admin/build_history.scala \ src/Pure/Admin/build_jcef.scala \ src/Pure/Admin/build_jdk.scala \ src/Pure/Admin/build_jedit.scala \ + src/Pure/Admin/build_lipics.scala \ src/Pure/Admin/build_log.scala \ src/Pure/Admin/build_minisat.scala \ src/Pure/Admin/build_pdfjs.scala \ @@ -251,7 +254,6 @@ src/Tools/jEdit/src/isabelle.scala \ src/Tools/jEdit/src/isabelle_encoding.scala \ src/Tools/jEdit/src/isabelle_export.scala \ - src/Tools/jEdit/src/isabelle_options.scala \ src/Tools/jEdit/src/isabelle_session.scala \ src/Tools/jEdit/src/isabelle_vfs.scala \ src/Tools/jEdit/src/jedit_bibtex.scala \ diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_Easychair/Document.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/Document.thy Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,64 @@ +theory Document + imports Main +begin + +section \Some section\ + +subsection \Some subsection\ + +subsection \Some subsubsection\ + +subsubsection \Some subsubsubsection\ + +paragraph \A paragraph.\ + +text \Informal bla bla.\ + +definition "foo = True" \ \side remark on \<^const>\foo\\ + +definition "bar = False" \ \side remark on \<^const>\bar\\ + +lemma foo unfolding foo_def .. + + +paragraph \Another paragraph.\ + +text \See also @{cite \\S3\ "isabelle-system"}.\ + + +section \Formal proof of Cantor's theorem\ + +text_raw \\isakeeptag{proof}\ +text \ + Cantor's Theorem states that there is no surjection from + a set to its powerset. The proof works by diagonalization. E.g.\ see + \<^item> \<^url>\http://mathworld.wolfram.com/CantorDiagonalMethod.html\ + \<^item> \<^url>\https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\ +\ + +theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x" +proof + assume "\f :: 'a \ 'a set. \A. \x. A = f x" + then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" .. + let ?D = "{x. x \ f x}" + from * obtain a where "?D = f a" by blast + moreover have "a \ ?D \ a \ f a" by blast + ultimately show False by blast +qed + + +subsection \Lorem ipsum dolor\ + +text \ + Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec id ipsum + sapien. Vivamus malesuada enim nibh, a tristique nisi sodales ac. Praesent + ut sem consectetur, interdum tellus ac, sodales nulla. Quisque vel diam at + risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus, + dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed + venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel. + Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices + sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla + efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit. +\ + +end diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_Easychair/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/document/root.bib Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,4 @@ +@manual{isabelle-system, + author = {Makarius Wenzel}, + title = {The {Isabelle} System Manual}, + note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}} diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_Easychair/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_Easychair/document/root.tex Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,31 @@ +\documentclass[a4paper,11pt]{easychair} +\usepackage{amssymb} +\usepackage{hyperref}\urlstyle{rm} + +\usepackage{isabelle,isabellesym}\isabellestyle{it} + +\isadroptag{theory} +\isafoldtag{proof} + + +\begin{document} + +\title{Isabelle document preparation with Easychair style} +\titlerunning{Easychair style} +\author{Makarius Wenzel} +\authorrunning{M. Wenzel} +\institute{\url{https://sketis.net}} +\maketitle + +\begin{abstract} +Isabelle is a formal document preparation system. This example shows how to +use it together with the Easychair style. See +\url{https://easychair.org/publications/for_authors} for further information. +\end{abstract} + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_FoilTeX/Document.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_FoilTeX/Document.thy Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,85 @@ +theory Document + imports Main +begin + +section \Abstract\ + +text \ + \small + Isabelle is a formal document preparation system. This example shows how to + use it together with Foil{\TeX} to produce slides in {\LaTeX}. See + \<^url>\https://ctan.org/pkg/foiltex\ for further information. +\ + + +chapter \Introduction\ + +section \Some slide\ + +paragraph \Point 1: + \plainstyle ABC\ + +text \ + \<^item> something + \<^item> to say \dots +\ + +paragraph \Point 2: + \plainstyle XYZ\ + +text \ + \<^item> more + \<^item> to say \dots +\ + + +section \Another slide\ + +paragraph \Key definitions:\ + +text \Informal bla bla.\ + +definition "foo = True" \ \side remark on \<^const>\foo\\ + +definition "bar = False" \ \side remark on \<^const>\bar\\ + +lemma foo unfolding foo_def .. + + +chapter \Application: Cantor's theorem\ + +section \Informal notes\ + +text_raw \\isakeeptag{proof}\ +text \ + Cantor's Theorem states that there is no surjection from + a set to its powerset. The proof works by diagonalization. E.g.\ see + \<^item> \<^url>\http://mathworld.wolfram.com/CantorDiagonalMethod.html\ + \<^item> \<^url>\https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\ +\ + +section \Formal proof\ + +theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x" +proof + assume "\f :: 'a \ 'a set. \A. \x. A = f x" + then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" .. + let ?D = "{x. x \ f x}" + from * obtain a where "?D = f a" by blast + moreover have "a \ ?D \ a \ f a" by blast + ultimately show False by blast +qed + + +chapter \Conclusion\ + +section \Lorem ipsum dolor\ + +text \ + \<^item> Lorem ipsum dolor sit amet, consectetur adipiscing elit. + \<^item> Donec id ipsum sapien. + \<^item> Vivamus malesuada enim nibh, a tristique nisi sodales ac. + \<^item> Praesent ut sem consectetur, interdum tellus ac, sodales nulla. +\ + +end diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_FoilTeX/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_FoilTeX/document/root.tex Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,65 @@ +\documentclass[a4paper,landscape]{foils} +\usepackage[utf8]{inputenc} +\usepackage{amssymb} +\usepackage[svgnames]{xcolor} +\usepackage{graphicx} +\usepackage{isabelle,isabellesym} +\usepackage{pdfsetup} + + +\makeatletter + +%colors +\newcommand{\titlestyle}{\color{DarkGreen}} +\newcommand{\hilitecolor}{\color{Blue}} +\newcommand{\hilite}[1]{{\hilitecolor#1}} +\newcommand{\red}[1]{{\color{Red}#1}} +\newcommand{\green}[1]{{\color{DarkGreen}#1}} + +%headings +\renewcommand{\isamarkupchapter}[1]{\newpage\thispagestyle{empty}\MyLogo{\let\\=\relax #1}\vspace*{0.4\textheight}\begin{center}\LARGE\bf\color{DarkGreen} #1\end{center}} +\renewcommand{\isamarkupsection}[1]{\foilhead{\color{DarkGreen}#1}} +\renewcommand\isamarkupparagraph{\@startsection{paragraph}{4}{0pt}{\bigskipamount}{0.5ex \@plus .1ex}{\normalsize\bf\color{DarkBlue}}} + +%item spacing +\renewcommand\@listIa{\leftmargin\leftmargini +\topsep 0\p@ \@plus 0.5\p@ \@minus 1\p@ +\parsep 2\p@ \@plus 1\p@ \@minus 1\p@ +\itemsep 2\p@ \@plus 1\p@ \@minus 0.5\p@} + +\makeatother + + +\parindent 0pt\parskip 0.5ex + +\urlstyle{sf} +\isabellestyle{it} +\MyLogo{} + +\newcommand{\plainstyle}{\normalsize\sf\color{black}} +\renewcommand{\isastyletext}{\normalsize\sf} +\renewcommand{\isastyletxt}{\sf} +\renewcommand{\isastylecmt}{\sf} + +\isadroptag{theory} +\isafoldtag{proof} + + +\begin{document} + +\title{\titlestyle Simple slides with with FoilTeX} +\author{Makarius Wenzel, Augsburg \\ \url{https://sketis.net}} +\date{} +\maketitle + +\vfill + +\begin{center} + \includegraphics[width=0.15\textwidth]{isabelle_logo} +\end{center} + +\vfill + +\input{session} + +\end{document} diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_LIPIcs/Document.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/Document.thy Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,64 @@ +theory Document + imports Main +begin + +section \Some section\ + +subsection \Some subsection\ + +subsection \Some subsubsection\ + +subsubsection \Some subsubsubsection\ + +paragraph \A paragraph.\ + +text \Informal bla bla.\ + +definition "foo = True" \ \side remark on \<^const>\foo\\ + +definition "bar = False" \ \side remark on \<^const>\bar\\ + +lemma foo unfolding foo_def .. + + +paragraph \Another paragraph.\ + +text \See also @{cite \\S3\ "isabelle-system"}.\ + + +section \Formal proof of Cantor's theorem\ + +text_raw \\isakeeptag{proof}\ +text \ + Cantor's Theorem states that there is no surjection from + a set to its powerset. The proof works by diagonalization. E.g.\ see + \<^item> \<^url>\http://mathworld.wolfram.com/CantorDiagonalMethod.html\ + \<^item> \<^url>\https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\ +\ + +theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x" +proof + assume "\f :: 'a \ 'a set. \A. \x. A = f x" + then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" .. + let ?D = "{x. x \ f x}" + from * obtain a where "?D = f a" by blast + moreover have "a \ ?D \ a \ f a" by blast + ultimately show False by blast +qed + + +subsection \Lorem ipsum dolor\ + +text \ + Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec id ipsum + sapien. Vivamus malesuada enim nibh, a tristique nisi sodales ac. Praesent + ut sem consectetur, interdum tellus ac, sodales nulla. Quisque vel diam at + risus tempus tempor eget a tortor. Suspendisse potenti. Nulla erat lacus, + dignissim sed volutpat nec, feugiat non leo. Nunc blandit et justo sed + venenatis. Donec scelerisque placerat magna, et congue nulla convallis vel. + Cras tristique dolor consequat dolor tristique rutrum. Suspendisse ultrices + sem nibh, et suscipit felis ultricies at. Aliquam venenatis est vel nulla + efficitur ornare. Lorem ipsum dolor sit amet, consectetur adipiscing elit. +\ + +end diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_LIPIcs/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/document/root.bib Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,4 @@ +@manual{isabelle-system, + author = {Makarius Wenzel}, + title = {The {Isabelle} System Manual}, + note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}} diff -r 8cb141384682 -r d9c78a18b44b src/Doc/Demo_LIPIcs/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Demo_LIPIcs/document/root.tex Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,59 @@ +\documentclass[a4paper,UKenglish,cleveref,autoref]{lipics-v2021} + +\usepackage{isabelle,isabellesym} +\isabellestyle{it} + +\isadroptag{theory} +\isafoldtag{proof} + + +\bibliographystyle{plainurl}% the mandatory bibstyle (e.g. from texlive-bibtex-extra) + +\title{Isabelle document preparation with Dagstuhl LIPIcs style} + +\author{Makarius Wenzel}{Augsburg, Germany \and \url{https://sketis.net}}{}{https://orcid.org/0000-0002-3753-8280}{} +\authorrunning{M. Wenzel} + +\Copyright{} + +\ccsdesc[100]{General and reference~General literature} +\ccsdesc[100]{General and reference} + +\keywords{Document preparation} + +\category{} + +\nolinenumbers + +%\hideLIPIcs %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository + +%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\EventEditors{John Q. Open and Joan R. Access} +\EventNoEds{2} +\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)} +\EventShortTitle{CVIT 2016} +\EventAcronym{CVIT} +\EventYear{2016} +\EventDate{December 24--27, 2016} +\EventLocation{Little Whinging, United Kingdom} +\EventLogo{} +\SeriesVolume{42} +\ArticleNo{23} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{document} + +\maketitle + +\begin{abstract} +Isabelle is a formal document preparation system. This example shows how to +use it together with the Dagstuhl LIPIcs style. See +\url{https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors} +for further information. +\end{abstract} + +\input{session} + +\bibliography{root} + +\end{document} diff -r 8cb141384682 -r d9c78a18b44b src/Doc/ROOT --- a/src/Doc/ROOT Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Doc/ROOT Mon Oct 31 21:58:08 2022 +0100 @@ -488,3 +488,38 @@ document_files "root.tex" "style.sty" + +session Demo_Easychair (doc) in "Demo_Easychair" = HOL + + options [document_variants = "demo_easychair"] + theories + Document + document_files (in "$ISABELLE_EASYCHAIR_HOME") + "easychair.cls" + document_files + "root.bib" + "root.tex" + +session Demo_FoilTeX (doc) in "Demo_FoilTeX" = HOL + + options [document_variants = "demo_foiltex", + document_build = "pdflatex", document_logo = "FoilTeX"] + theories + Document + document_files (in "$ISABELLE_FOILTEX_HOME") + "fltfonts.def" + "foil20.clo" + "foils.cls" + document_files + "root.tex" + +session Demo_LIPIcs (doc) in "Demo_LIPIcs" = HOL + + options [document_variants = "demo_lipics", + document_build = "pdflatex", document_heading_prefix = "", document_comment_latex] + theories + Document + document_files (in "$ISABELLE_LIPICS_HOME") + "cc-by.pdf" + "lipics-logo-bw.pdf" + "lipics-v2021.cls" + document_files + "root.bib" + "root.tex" diff -r 8cb141384682 -r d9c78a18b44b src/Pure/Admin/build_easychair.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_easychair.scala Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,108 @@ +/* Title: Pure/Admin/build_easychair.scala + Author: Makarius + +Build Isabelle component for Easychair style. + +See also https://easychair.org/publications/for_authors +*/ + +package isabelle + + +object Build_Easychair { + /* build easychair component */ + + val default_url = "https://easychair.org/publications/easychair.zip" + + def build_easychair( + download_url: String = default_url, + target_dir: Path = Path.current, + progress: Progress = new Progress + ): Unit = { + Isabelle_System.require_command("unzip", test = "-h") + + Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => + Isabelle_System.with_tmp_dir("download") { download_dir => + + /* download */ + + Isabelle_System.download_file(download_url, download_file, progress = progress) + Isabelle_System.bash("unzip -x " + File.bash_path(download_file), + cwd = download_dir.file).check + + val easychair_dir = + File.read_dir(download_dir) match { + case List(name) => download_dir + Path.explode(name) + case bad => + error("Expected exactly one directory entry in " + download_file + + bad.mkString("\n", "\n ", "")) + } + + + /* component */ + + val version = + Library.try_unprefix("EasyChair", easychair_dir.file_name) + .getOrElse("Failed to detect version from " + quote(easychair_dir.file_name)) + + val component = "easychair-" + version + val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) + progress.echo("Component " + component_dir) + + component_dir.file.delete + Isabelle_System.copy_dir(easychair_dir, component_dir) + + + /* settings */ + + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) + File.write(etc_dir + Path.basic("settings"), + """# -*- shell-script -*- :mode=shellscript: + +ISABELLE_EASYCHAIR_HOME="$COMPONENT" +""") + + + /* README */ + + File.write(component_dir + Path.basic("README"), + """This is the Easychair style for authors from +""" + download_url + """ + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") + } + } + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("build_easychair", "build component for Easychair style", + Scala_Project.here, + { args => + var target_dir = Path.current + var download_url = default_url + + val getopts = Getopts(""" +Usage: isabelle build_easychair [OPTIONS] + + Options are: + -D DIR target directory (default ".") + -U URL download URL (default: """" + default_url + """") + + Build component for Easychair style. +""", + "D:" -> (arg => target_dir = Path.explode(arg)), + "U:" -> (arg => download_url = arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val progress = new Console_Progress() + + build_easychair(download_url = download_url, target_dir = target_dir, progress = progress) + }) +} diff -r 8cb141384682 -r d9c78a18b44b src/Pure/Admin/build_foiltex.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_foiltex.scala Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,117 @@ +/* Title: Pure/Admin/build_foiltex.scala + Author: Makarius + +Build Isabelle component for FoilTeX. + +See also https://ctan.org/pkg/foiltex +*/ + +package isabelle + + +object Build_Foiltex { + /* build FoilTeX component */ + + val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip" + + def build_foiltex( + download_url: String = default_url, + target_dir: Path = Path.current, + progress: Progress = new Progress + ): Unit = { + Isabelle_System.require_command("unzip", test = "-h") + + Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => + Isabelle_System.with_tmp_dir("download") { download_dir => + + /* download */ + + Isabelle_System.download_file(download_url, download_file, progress = progress) + Isabelle_System.bash("unzip -x " + File.bash_path(download_file), + cwd = download_dir.file).check + + val foiltex_dir = + File.read_dir(download_dir) match { + case List(name) => download_dir + Path.explode(name) + case bad => + error("Expected exactly one directory entry in " + download_file + + bad.mkString("\n", "\n ", "")) + } + + val README = Path.explode("README") + val README_flt = Path.explode("README.flt") + Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt) + + Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check + + + /* component */ + + val version = { + val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r + split_lines(File.read(foiltex_dir + README_flt)) + .collectFirst({ case Version(v) => v }) + .getOrElse(error("Failed to detect version in " + README_flt)) + } + + val component = "foiltex-" + version + val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) + progress.echo("Component " + component_dir) + + component_dir.file.delete + Isabelle_System.copy_dir(foiltex_dir, component_dir) + + + /* settings */ + + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) + File.write(etc_dir + Path.basic("settings"), + """# -*- shell-script -*- :mode=shellscript: + +ISABELLE_FOILTEX_HOME="$COMPONENT" +""") + + + /* README */ + + File.write(component_dir + Path.basic("README"), + """This is FoilTeX from +""" + download_url + """ + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") + } + } + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("build_foiltex", "build component for FoilTeX", + Scala_Project.here, + { args => + var target_dir = Path.current + var download_url = default_url + + val getopts = Getopts(""" +Usage: isabelle build_foiltex [OPTIONS] + + Options are: + -D DIR target directory (default ".") + -U URL download URL (default: """" + default_url + """") + + Build component for FoilTeX: slides in LaTeX. +""", + "D:" -> (arg => target_dir = Path.explode(arg)), + "U:" -> (arg => download_url = arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val progress = new Console_Progress() + + build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress) + }) +} diff -r 8cb141384682 -r d9c78a18b44b src/Pure/Admin/build_lipics.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Admin/build_lipics.scala Mon Oct 31 21:58:08 2022 +0100 @@ -0,0 +1,107 @@ +/* Title: Pure/Admin/build_lipics.scala + Author: Makarius + +Build Isabelle component for Dagstuhl LIPIcs style. + +See also: + + - https://github.com/dagstuhl-publishing/styles + - https://submission.dagstuhl.de/documentation/authors + - https://www.dagstuhl.de/en/publications/lipics +*/ + +package isabelle + + +object Build_LIPIcs { + /* build lipics component */ + + val default_url = "https://github.com/dagstuhl-publishing/styles/archive/refs/tags/v2021.1.2.tar.gz" + + def build_lipics( + download_url: String = default_url, + target_dir: Path = Path.current, + progress: Progress = new Progress + ): Unit = { + Isabelle_System.with_tmp_file("download", ext = "tar.gz") { download_file => + Isabelle_System.with_tmp_dir("download") { download_dir => + + /* download */ + + Isabelle_System.download_file(download_url, download_file, progress = progress) + Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), + dir = download_dir, strip = 1).check + + val lipics_dir = download_dir + Path.explode("LIPIcs/authors") + + + /* component */ + + val version = { + val Version = """^*.* v(.*)$""".r + val changelog = Path.explode("CHANGELOG.md") + split_lines(File.read(lipics_dir + changelog)) + .collectFirst({ case Version(v) => v }) + .getOrElse(error("Failed to detect version in " + changelog)) + } + + val component = "lipics-" + version + val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) + progress.echo("Component " + component_dir) + + Isabelle_System.copy_dir(lipics_dir, component_dir) + + + /* settings */ + + val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) + File.write(etc_dir + Path.basic("settings"), + """# -*- shell-script -*- :mode=shellscript: + +ISABELLE_LIPICS_HOME="$COMPONENT/authors" +""") + + + /* README */ + + File.write(component_dir + Path.basic("README"), + """This is the Dagstuhl LIPIcs style for authors from +""" + download_url + """ + + + Makarius + """ + Date.Format.date(Date.now()) + "\n") + } + } + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("build_lipics", "build component for Dagstuhl LIPIcs style", + Scala_Project.here, + { args => + var target_dir = Path.current + var download_url = default_url + + val getopts = Getopts(""" +Usage: isabelle build_lipics [OPTIONS] + + Options are: + -D DIR target directory (default ".") + -U URL download URL (default: """" + default_url + """") + + Build component for Dagstuhl LIPIcs style. +""", + "D:" -> (arg => target_dir = Path.explode(arg)), + "U:" -> (arg => download_url = arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val progress = new Console_Progress() + + build_lipics(download_url = download_url, target_dir = target_dir, progress = progress) + }) +} diff -r 8cb141384682 -r d9c78a18b44b src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Pure/PIDE/markup.ML Mon Oct 31 21:58:08 2022 +0100 @@ -237,7 +237,7 @@ val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string - val functionN: string + val function: string -> Properties.entry val ML_statistics: {pid: int, stats_dir: string} -> Properties.T val commands_accepted: Properties.T val assign_update: Properties.T @@ -250,7 +250,6 @@ val session_timing: Properties.entry val loading_theory: string -> Properties.T val build_session_finished: Properties.T - val print_operationsN: string val print_operations: Properties.T val exportN: string type export_args = @@ -751,34 +750,33 @@ (* protocol message functions *) -val functionN = "function" +fun function name = ("function", name); fun ML_statistics {pid, stats_dir} = - [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; + [function "ML_statistics", ("pid", Value.print_int pid), ("stats_dir", stats_dir)]; -val commands_accepted = [(functionN, "commands_accepted")]; +val commands_accepted = [function "commands_accepted"]; -val assign_update = [(functionN, "assign_update")]; -val removed_versions = [(functionN, "removed_versions")]; +val assign_update = [function "assign_update"]; +val removed_versions = [function "removed_versions"]; -fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; +fun invoke_scala name id = [function "invoke_scala", (nameN, name), (idN, id)]; -fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; - -val task_statistics = (functionN, "task_statistics"); +fun cancel_scala id = [function "cancel_scala", (idN, id)]; -val command_timing = (functionN, "command_timing"); +val task_statistics = function "task_statistics"; -val theory_timing = (functionN, "theory_timing"); +val command_timing = function "command_timing"; -val session_timing = (functionN, "session_timing"); +val theory_timing = function "theory_timing"; -fun loading_theory name = [("function", "loading_theory"), (nameN, name)]; +val session_timing = function "session_timing"; + +fun loading_theory name = [function "loading_theory", (nameN, name)]; -val build_session_finished = [("function", "build_session_finished")]; +val build_session_finished = [function "build_session_finished"]; -val print_operationsN = "print_operations"; -val print_operations = [(functionN, print_operationsN)]; +val print_operations = [function "print_operations"]; (* export *) @@ -795,7 +793,7 @@ strict: bool}; fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = - [(functionN, exportN), + [function exportN, (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), @@ -807,8 +805,8 @@ (* debugger *) -fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; -fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; +fun debugger_state name = [function "debugger_state", (nameN, name)]; +fun debugger_output name = [function "debugger_output", (nameN, name)]; (* simplifier trace *) @@ -821,7 +819,7 @@ val simp_trace_hintN = "simp_trace_hint"; val simp_trace_ignoreN = "simp_trace_ignore"; -fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; +fun simp_trace_cancel i = [function "simp_trace_cancel", (serialN, Value.print_int i)]; diff -r 8cb141384682 -r d9c78a18b44b src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Pure/PIDE/markup.scala Mon Oct 31 21:58:08 2022 +0100 @@ -612,13 +612,13 @@ val FUNCTION = "function" class Function(val name: String) { - val PROPERTY: Properties.Entry = (FUNCTION, name) + val THIS: Properties.Entry = (FUNCTION, name) } class Properties_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[Properties.T] = props match { - case PROPERTY :: args => Some(args) + case THIS :: args => Some(args) case _ => None } } @@ -626,7 +626,7 @@ class Name_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[String] = props match { - case List(PROPERTY, (NAME, a)) => Some(a) + case List(THIS, (NAME, a)) => Some(a) case _ => None } } @@ -634,7 +634,7 @@ object ML_Statistics extends Function("ML_statistics") { def unapply(props: Properties.T): Option[(Long, String)] = props match { - case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => + case List(THIS, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => Some((pid, stats_dir)) case _ => None } @@ -660,7 +660,7 @@ object Invoke_Scala extends Function("invoke_scala") { def unapply(props: Properties.T): Option[(String, String)] = props match { - case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id)) + case List(THIS, (NAME, name), (ID, id)) => Some((name, id)) case _ => None } } @@ -668,7 +668,7 @@ object Cancel_Scala extends Function("cancel_scala") { def unapply(props: Properties.T): Option[String] = props match { - case List(PROPERTY, (ID, id)) => Some(id) + case List(THIS, (ID, id)) => Some(id) case _ => None } } diff -r 8cb141384682 -r d9c78a18b44b src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Pure/PIDE/session.scala Mon Oct 31 21:58:08 2022 +0100 @@ -487,7 +487,7 @@ try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } - case List(Markup.Commands_Accepted.PROPERTY) => + case List(Markup.Commands_Accepted.THIS) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => @@ -495,7 +495,7 @@ case _ => bad_output() } - case List(Markup.Assign_Update.PROPERTY) => + case List(Markup.Assign_Update.THIS) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { @@ -509,7 +509,7 @@ } delay_prune.invoke() - case List(Markup.Removed_Versions.PROPERTY) => + case List(Markup.Removed_Versions.THIS) => msg.text match { case Protocol.Removed(removed) => try { diff -r 8cb141384682 -r d9c78a18b44b src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Pure/System/isabelle_tool.scala Mon Oct 31 21:58:08 2022 +0100 @@ -159,10 +159,13 @@ Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_E.isabelle_tool, + Build_Easychair.isabelle_tool, + Build_Foiltex.isabelle_tool, Build_Fonts.isabelle_tool, Build_JCEF.isabelle_tool, Build_JDK.isabelle_tool, Build_JEdit.isabelle_tool, + Build_LIPIcs.isabelle_tool, Build_Minisat.isabelle_tool, Build_PDFjs.isabelle_tool, Build_PolyML.isabelle_tool1, diff -r 8cb141384682 -r d9c78a18b44b src/Pure/Tools/build_docker.scala --- a/src/Pure/Tools/build_docker.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Pure/Tools/build_docker.scala Mon Oct 31 21:58:08 2022 +0100 @@ -20,7 +20,12 @@ val package_collections: Map[String, List[String]] = Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), "latex" -> - List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science")) + List( + "texlive-bibtex-extra", + "texlive-fonts-extra", + "texlive-font-utils", + "texlive-latex-extra", + "texlive-science")) def all_packages: List[String] = packages ::: package_collections.valuesIterator.flatten.toList diff -r 8cb141384682 -r d9c78a18b44b src/Tools/jEdit/jedit_main/plugin.props --- a/src/Tools/jEdit/jedit_main/plugin.props Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Tools/jEdit/jedit_main/plugin.props Mon Oct 31 21:58:08 2022 +0100 @@ -23,9 +23,9 @@ #options plugin.isabelle.jedit_main.Plugin.option-group=isabelle-general isabelle-rendering options.isabelle-general.label=General -options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1(); +options.isabelle-general.code=new isabelle.jedit.JEdit_Options$Isabelle_General_Options(); options.isabelle-rendering.label=Rendering -options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2(); +options.isabelle-rendering.code=new isabelle.jedit.JEdit_Options$Isabelle_Rendering_Options(); #menu actions and dockables plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle diff -r 8cb141384682 -r d9c78a18b44b src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Fri Oct 28 06:34:26 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -/* Title: Tools/jEdit/src/isabelle_options.scala - Author: Makarius - -Editor pane for plugin options. -*/ - -package isabelle.jedit - - -import isabelle._ - -import org.gjt.sp.jedit.{jEdit, AbstractOptionPane} - - -abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) { - protected val components: List[(String, List[Option_Component])] - - override def _init(): Unit = { - val dummy_property = "options.isabelle.dummy" - - for ((s, cs) <- components) { - if (s != "") { - jEdit.setProperty(dummy_property, s) - addSeparator(dummy_property) - jEdit.setProperty(dummy_property, null) - } - cs.foreach(c => addComponent(c.title, c.peer)) - } - } - - override def _save(): Unit = { - for ((_, cs) <- components) cs.foreach(_.save()) - } -} - - -class Isabelle_Options1 extends Isabelle_Options("isabelle-general") { - val options: JEdit_Options = PIDE.options - - private val predefined = - List(JEdit_Sessions.logic_selector(options), - JEdit_Spell_Checker.dictionaries_selector()) - - protected val components = - options.make_components(predefined, - (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet) -} - - -class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") { - private val predefined = - (for { - (name, opt) <- PIDE.options.value.opt_iterator - if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION) - } yield PIDE.options.make_color_component(opt)).toList - - assert(predefined.nonEmpty) - - protected val components = PIDE.options.make_components(predefined, _ => false) -} diff -r 8cb141384682 -r d9c78a18b44b src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Tools/jEdit/src/jedit_options.scala Mon Oct 31 21:58:08 2022 +0100 @@ -16,20 +16,10 @@ import scala.swing.{Component, CheckBox, TextArea} import org.gjt.sp.jedit.gui.ColorWellButton +import org.gjt.sp.jedit.{jEdit, AbstractOptionPane} -trait Option_Component extends Component { - val title: String - def load(): Unit - def save(): Unit -} - object JEdit_Options { - /* sections */ - - val RENDERING_SECTION = "Rendering of Document Content" - - /* typed access and GUI components */ class Access[A](access: Options.Access_Variable[A], val name: String) { @@ -81,30 +71,86 @@ tooltip = "Output of proof state (normally shown on State panel)" } } + + + /* editor pane for plugin options */ + + trait Entry extends Component { + val title: String + def load(): Unit + def save(): Unit + } + + abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) { + protected val components: List[(String, List[Entry])] + + override def _init(): Unit = { + val dummy_property = "options.isabelle.dummy" + + for ((s, cs) <- components) { + if (s.nonEmpty) { + jEdit.setProperty(dummy_property, s) + addSeparator(dummy_property) + jEdit.setProperty(dummy_property, null) + } + for (c <- cs) addComponent(c.title, c.peer) + } + } + + override def _save(): Unit = { + for ((_, cs) <- components; c <- cs) c.save() + } + } + + class Isabelle_General_Options extends Isabelle_Options("isabelle-general") { + val options: JEdit_Options = PIDE.options + + private val predefined = + List(JEdit_Sessions.logic_selector(options), + JEdit_Spell_Checker.dictionaries_selector()) + + protected val components: List[(String, List[Entry])] = + options.make_components(predefined, + (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet) + } + + class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") { + private val predefined = + (for { + (name, opt) <- PIDE.options.value.opt_iterator + if name.endsWith("_color") && opt.section == "Rendering of Document Content" + } yield PIDE.options.make_color_component(opt)).toList + + assert(predefined.nonEmpty) + + protected val components: List[(String, List[Entry])] = + PIDE.options.make_components(predefined, _ => false) + } } class JEdit_Options(init_options: Options) extends Options_Variable(init_options) { def color_value(s: String): Color = Color_Value(string(s)) - def make_color_component(opt: Options.Opt): Option_Component = { + def make_color_component(opt: Options.Opt): JEdit_Options.Entry = { GUI_Thread.require {} val opt_name = opt.name val opt_title = opt.title("jedit") val button = new ColorWellButton(Color_Value(opt.value)) - val component = new Component with Option_Component { - override lazy val peer: JComponent = button - name = opt_name - val title: String = opt_title - def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name))) - def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor) - } + val component = + new Component with JEdit_Options.Entry { + override lazy val peer: JComponent = button + name = opt_name + val title: String = opt_title + def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name))) + def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor) + } component.tooltip = GUI.tooltip_lines(opt.print_default) component } - def make_component(opt: Options.Opt): Option_Component = { + def make_component(opt: Options.Opt): JEdit_Options.Entry = { GUI_Thread.require {} val opt_name = opt.name @@ -112,7 +158,7 @@ val component = if (opt.typ == Options.Bool) - new CheckBox with Option_Component { + new CheckBox with JEdit_Options.Entry { name = opt_name val title: String = opt_title def load(): Unit = selected = bool(opt_name) @@ -121,7 +167,7 @@ else { val default_font = GUI.copy_font(UIManager.getFont("TextField.font")) val text_area = - new TextArea with Option_Component { + new TextArea with JEdit_Options.Entry { if (default_font != null) font = default_font name = opt_name val title: String = opt_title @@ -149,10 +195,10 @@ } def make_components( - predefined: List[Option_Component], + predefined: List[JEdit_Options.Entry], filter: String => Boolean - ) : List[(String, List[Option_Component])] = { - def mk_component(opt: Options.Opt): List[Option_Component] = + ) : List[(String, List[JEdit_Options.Entry])] = { + def mk_component(opt: Options.Opt): List[JEdit_Options.Entry] = predefined.find(opt.name == _.name) match { case Some(c) => List(c) case None => if (filter(opt.name)) List(make_component(opt)) else Nil @@ -162,4 +208,3 @@ .filterNot(_._2.isEmpty) } } - diff -r 8cb141384682 -r d9c78a18b44b src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Mon Oct 31 21:58:08 2022 +0100 @@ -73,7 +73,7 @@ override def toString: String = proper_string(description) getOrElse name } - def logic_selector(options: Options_Variable, autosave: Boolean = false): Option_Component = { + def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = { GUI_Thread.require {} val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")") @@ -85,7 +85,8 @@ (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name)) } - new GUI.Selector[Logic_Entry](default_entry :: session_entries) with Option_Component { + new GUI.Selector[Logic_Entry](default_entry :: session_entries) + with JEdit_Options.Entry { name = jedit_logic_option tooltip = "Logic session name (change requires restart)" val title = "Logic" diff -r 8cb141384682 -r d9c78a18b44b src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala Fri Oct 28 06:34:26 2022 +0000 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Oct 31 21:58:08 2022 +0100 @@ -79,13 +79,13 @@ /* dictionaries */ - def dictionaries_selector(): Option_Component = { + def dictionaries_selector(): JEdit_Options.Entry = { GUI_Thread.require {} val option_name = "spell_checker_dictionary" val opt = PIDE.options.value.check_name(option_name) - new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with Option_Component { + new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with JEdit_Options.Entry { name = option_name tooltip = GUI.tooltip_lines(opt.print_default) val title = opt.title()