| author | wenzelm |
| Sun, 24 Jan 2021 19:34:37 +0100 | |
| changeset 73183 | ebf7babc05ce |
| parent 73142 | 0398f18ec76c (current diff) |
| parent 73182 | a8a8bc42d552 (diff) |
| child 73184 | a5998396051e |
--- a/.hgtags Thu Jan 21 18:18:19 2021 +0100 +++ b/.hgtags Sun Jan 24 19:34:37 2021 +0100 @@ -40,3 +40,4 @@ 21ff9c1a464494b3a61c3538650664cc1b42c0cb Isabelle2021-RC0 d4b67dc6f4ebd5f0fbd4ed1cccd0cc32c344d122 Isabelle2021-RC1 802647edfe7be4478ca47a6e54e4d73733347e02 Isabelle2021-RC2 +02422c9add5e1c608290e48f3f0815c93ab00c1d Isabelle2021-RC3
--- a/ANNOUNCE Thu Jan 21 18:18:19 2021 +0100 +++ b/ANNOUNCE Sun Jan 24 19:34:37 2021 +0100 @@ -12,7 +12,7 @@ * Isabelle/jEdit: improved monitoring of Java and ML process. -* Isabelle/jEdit: look-and-feel and IDE feedback improvements. +* Isabelle/jEdit: improved look-and-feel and IDE feedback. * Pure: improved handling of named contexts and local syntax bundles. @@ -28,7 +28,7 @@ * System: support for Isabelle/Scala services defined in user-space. -* Experimental support for ARM64 platform on Linux and macOS (Apple Silicon). +* Partial support for ARM64 platform on Linux and macOS (Apple Silicon). You may get Isabelle2021 from the following mirror sites:
--- a/Admin/components/components.sha1 Thu Jan 21 18:18:19 2021 +0100 +++ b/Admin/components/components.sha1 Sun Jan 24 19:34:37 2021 +0100 @@ -82,6 +82,7 @@ ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz 7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz +d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz 20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz 736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz @@ -209,6 +210,9 @@ ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz 400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz 3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz +0fbc826e4fcb95bb9e1814642f7fce788e7fe1c3 naproche-20210122-1.tar.gz +eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz +edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz 26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz
--- a/Admin/components/main Thu Jan 21 18:18:19 2021 +0100 +++ b/Admin/components/main Sun Jan 24 19:34:37 2021 +0100 @@ -4,7 +4,7 @@ csdp-6.1.1 cvc4-1.8 e-2.5-1 -flatlaf-0.46-1 +flatlaf-1.0-rc1 isabelle_fonts-20190717 jdk-15.0.1+9 jedit_build-20201223
--- a/NEWS Thu Jan 21 18:18:19 2021 +0100 +++ b/NEWS Sun Jan 24 19:34:37 2021 +0100 @@ -4,11 +4,6 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) -New in this Isabelle version ----------------------------- - - - New in Isabelle2021 (February 2021) ----------------------------------- @@ -62,12 +57,16 @@ * Update to jedit-5.6.0, the latest release. This version works properly on macOS by default, without the special MacOSX plugin. -* On macOS Big Sur full-screen mode works requires to change "System -Preferences / General / Prefer tabs: in full screen" to never. - * Action "full-screen-mode" (shortcut F11 or S+F11) has been modified for better approximate window size on macOS and Linux/X11. +* Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode, +but non-native look-and-feel (FlatLaf). + +* IDE support for Naproche-SAD: Proof Checking of Natural Mathematical +Documents. See also $NAPROCHE_HOME/examples for files with .ftl or +.ftl.tex extension. + *** Document preparation *** @@ -293,6 +292,10 @@ (for DVI documents) has been discontinued. Former option -n has been turned into -o with explicit file name. Minor INCOMPATIBILITY. +* The command-line tool "isabelle components" supports new options -u +and -x to manage $ISABELLE_HOME_USER/etc/components without manual +editing of Isabelle configuration files. + * The shell function "isabelle_directory" (within etc/settings of components) augments the list of special directories for persistent symbolic path names. This improves portability of heap images and @@ -364,6 +367,10 @@ * Experimental support for arm64-linux platform. The reference platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit). +* Partial support for arm64-darwin (Apple Silicon): most x86_64 +executables work well with runtime translation by Rosetta, but +occasional problems remain (e.g. external provers). + New in Isabelle2020 (April 2020)
--- a/etc/settings Thu Jan 21 18:18:19 2021 +0100 +++ b/etc/settings Sun Jan 24 19:34:37 2021 +0100 @@ -159,7 +159,7 @@ ISABELLE_STACK_ROOT="$USER_HOME/.stack" -ISABELLE_STACK_RESOLVER="lts-16.12" +ISABELLE_STACK_RESOLVER="lts-16.31" ISABELLE_GHC_VERSION="ghc-8.8.4"
--- a/lib/Tools/components Thu Jan 21 18:18:19 2021 +0100 +++ b/lib/Tools/components Sun Jan 24 19:34:37 2021 +0100 @@ -19,11 +19,15 @@ echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)" echo " -a resolve all missing components" echo " -l list status" + echo " -u DIR update \$ISABELLE_HOME_USER/components: add directory" + echo " -x DIR update \$ISABELLE_HOME_USER/components: remove directory" echo - echo " Resolve Isabelle components via download and installation." - echo " COMPONENTS are identified via base name." + echo " Resolve Isabelle components via download and installation: given COMPONENTS" + echo " are identified via base name. Further operations manage etc/settings and" + echo " etc/components in \$ISABELLE_HOME_USER." echo echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\"" + echo " ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\"" echo exit 1 } @@ -43,8 +47,9 @@ COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY" ALL_MISSING="" LIST_ONLY="" +declare -a UPDATE_COMPONENTS=() -while getopts "IR:al" OPT +while getopts "IR:alu:x:" OPT do case "$OPT" in I) @@ -59,6 +64,12 @@ l) LIST_ONLY="true" ;; + u) + UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG" + ;; + x) + UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG" + ;; \?) usage ;; @@ -70,7 +81,7 @@ # args -[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage +[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && usage if [ -z "$ALL_MISSING" ]; then splitarray ":" "$@" @@ -112,6 +123,9 @@ echo echo "Missing components:" for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done +elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then + isabelle_admin_build jars || exit $? + exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}" else for NAME in "${SELECTED_COMPONENTS[@]}" do
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/java-gui-setup Sun Jan 24 19:34:37 2021 +0100 @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# +# java-gui-setup --- platform-specific setup for Java/Swing GUI applications + +if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] +then + JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" + JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" + defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || + defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null +fi
--- a/src/Doc/JEdit/JEdit.thy Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Doc/JEdit/JEdit.thy Sun Jan 24 19:34:37 2021 +0100 @@ -73,11 +73,11 @@ \end{figure} Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for - the jEdit text editor, while preserving its general look-and-feel as far as - possible. The main plugin is called ``Isabelle'' and has its own menu - \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several actions and add-on panels (see - also \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ - Isabelle\<close> (see also \secref{sec:options}). + the jEdit text editor, while preserving its overall look-and-feel. The main + plugin is called ``Isabelle'' and has its own menu \<^emph>\<open>Plugins~/ Isabelle\<close> + with access to several actions and add-on panels (see also + \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<close> + (see also \secref{sec:options}). The options allow to specify a logic session name, but the same selector is also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After @@ -305,7 +305,7 @@ The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a different server name. The default server name is the official distribution - name (e.g.\ \<^verbatim>\<open>Isabelle2020\<close>). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\<open>Isabelle2021\<close>). Thus @{tool jedit_client} can connect to the Isabelle desktop application without further options. The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system @@ -320,56 +320,54 @@ section \<open>GUI rendering\<close> -subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close> +text \<open> + Isabelle/jEdit is a classic Java/AWT/Swing application: its GUI rendering + usually works well, but there are technical side-conditions on the Java + window system and graphics engine. When researching problems and solutions + on the Web, it often helps to include other well-known Swing applications, + notably IntelliJ IDEA and Netbeans. +\<close> + + +subsection \<open>Portable and scalable look-and-feel\<close> text \<open> - jEdit is a Java/AWT/Swing application with the ambition to support - ``native'' look-and-feel on all platforms, within the limits of what Java - provider and major operating systems allow (see also \secref{sec:problems}). - - Isabelle/jEdit enables platform-specific look-and-feel by default as - follows. - - \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default. - - The Linux-specific \<^emph>\<open>GTK+\<close> look-and-feel often works, but the overall GTK - theme and options need to be selected to suite Java/AWT/Swing. Note that - the Java Virtual Machine has no direct influence of GTK rendering: it - happens within external C libraries. - - \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> look-and-feel is used by default. - - \<^descr>[macOS:] Regular \<^emph>\<open>Mac OS X\<close> look-and-feel is used by default. - - Users may experiment with different Swing look-and-feels, but need to keep - in mind that this extra variance of GUI functionality often causes problems. - The platform-independent \<^emph>\<open>Metal\<close> look-and-feel should work smoothly on all - platforms, although its is technically and stylistically outdated. - - Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the - GUI only partially: a proper restart of Isabelle/jEdit is usually required. + In the past, \<^emph>\<open>system look-and-feels\<close> tried hard to imitate native GUI + elements on specific platforms (Windows, macOS/Aqua, Linux/GTK+), but many + technical problems have accumulated in recent years (e.g.\ see + \secref{sec:problems}). + + In 2021, we are de-facto back to \<^emph>\<open>portable look-and-feels\<close>, which also + happen to be \emph{scalable} on high-resolution displays: + + \<^item> \<^verbatim>\<open>FlatLaf Light\<close> is the default for Isabelle/jEdit on all platforms. It + generally looks good and adapts itself pretty well to high-resolution + displays. + + \<^item> \<^verbatim>\<open>FlatLaf Dark\<close> is an alternative, but it requires further changes of + editor colors by the user (or by the jEdit plugin \<^verbatim>\<open>Editor Scheme\<close>). Also + note that Isabelle/PIDE has its own extensive set of rendering options + that need to be revisited. + + \<^item> \<^verbatim>\<open>Metal\<close> still works smoothly, although it is stylistically outdated. It + can accommodate high-resolution displays via font properties (see below). + + Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> often updates + the GUI only partially: a full restart of Isabelle/jEdit is required to see + the true effect. \<close> -subsection \<open>Displays with high resolution \label{sec:hdpi}\<close> +subsection \<open>Adjusting fonts\<close> text \<open> - In 2020, we usually see displays with high resolution like ``Ultra HD'' / - ``4K'' at $3840 \times 2160$, or more. Old ``Full HD'' displays at $1920 - \times 1080$ pixels are still being used, but Java 11 font-rendering might - look bad on it. GUI layouts are lagging behind the high resolution trends, - and implicitly assume very old-fashioned $1024 \times 768$ or $1280 \times - 1024$ screens and fonts with 12 or 14 pixels. Java and jEdit do provide - reasonable support for high resolution, but this requires manual - adjustments as described below. - - \<^medskip> The \<^bold>\<open>operating-system\<close> often provides some configuration for global - scaling of text fonts, e.g.\ to enlarge it uniformly by $200\%$. This - impacts regular GUI elements, when used with native look-and-feel: Linux - \<^emph>\<open>GTK+\<close>, \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is - possible to use the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and change - its main font sizes via jEdit options explained below. The Isabelle/jEdit - \<^bold>\<open>application\<close> provides further options to adjust font sizes in particular + The preferred font family for Isabelle/jEdit is \<^verbatim>\<open>Isabelle DejaVu\<close>: it is + used by default for the main text area and various GUI elements. The default + font sizes attempt to deliver a usable application for common display types, + such as ``Full HD'' at $1920 \times 1080$ and ``Ultra HD'' at $3840 \times + 2160$. + + \<^medskip> Isabelle/jEdit provides various options to adjust font sizes in particular GUI elements. Here is a summary of all relevant font properties: \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font, @@ -383,7 +381,7 @@ \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font - for the \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}). + for the \<^emph>\<open>Metal\<close> look-and-feel. \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\ @@ -391,19 +389,6 @@ \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font, e.g.\ relevant for Isabelle/Scala command-line. - - In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured - with custom fonts at 36 pixels, and the main text area and console at 40 - pixels. This leads to fairly good rendering quality, despite the - old-fashioned appearance of \<^emph>\<open>Metal\<close>. - - \begin{sidewaysfigure}[!htb] - \begin{center} - \includegraphics[width=\textwidth]{isabelle-jedit-hdpi} - \end{center} - \caption{Metal look-and-feel with custom fonts for high resolution} - \label{fig:isabelle-jedit-hdpi} - \end{sidewaysfigure} \<close> @@ -715,10 +700,9 @@ subsection \<open>PIDE resources via virtual file-systems\<close> text \<open> - The jEdit file browser is docked by default, e.g. see - \figref{fig:isabelle-jedit-hdpi} (left docking area). It provides immediate - access to the local file-system, as well as important Isabelle resources via - the \<^emph>\<open>Favorites\<close> menu. Environment variables like \<^verbatim>\<open>$ISABELLE_HOME\<close> are + The jEdit file browser is docked by default. It provides immediate access to + the local file-system, as well as important Isabelle resources via the + \<^emph>\<open>Favorites\<close> menu. Environment variables like \<^verbatim>\<open>$ISABELLE_HOME\<close> are discussed in \secref{sec:local-files}. Virtual file-systems are more special: the idea is to present structured information like a directory tree. The following URLs are offered in the \<^emph>\<open>Favorites\<close> menu, or by @@ -2188,13 +2172,6 @@ \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to the national keyboard layout, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones. - \<^item> \<^bold>\<open>Problem:\<close> On macOS Big Sur full-screen mode causes problems with dialog windows - (e.g. \<^emph>\<open>Search and Replace\<close> or \<^emph>\<open>Hypersearch Results\<close>). - - \<^bold>\<open>Workaround:\<close> Go to \<^emph>\<open>System Preferences / General\<close> and change the default - ``\<^emph>\<open>Prefer tabs: \<^bold>\<open>in full screen\<close> when opening documents\<close>'' to - ``\<^emph>\<open>\<^bold>\<open>never\<close>\<close>''. - \<^item> \<^bold>\<open>Problem:\<close> On macOS with native Apple look-and-feel, some exotic national keyboards may cause a conflict of menu accelerator keys with regular jEdit key bindings. This leads to duplicate execution of the @@ -2255,15 +2232,7 @@ For the latter platforms, it is approximated by educated guesses on the window size (excluding the macOS menu bar). - \<^bold>\<open>Workaround:\<close> Use native full-screen control of the macOS window manager, - unless it is macOS 11.1 (Big Sur). - - \<^item> \<^bold>\<open>Problem:\<close> Native full-screen mode on macOS 11.1 is incompatible with - Java window management: it puts dialog windows (Search, Hypersearch, etc.) - into an unusable state. - - \<^bold>\<open>Workaround:\<close> use the approximative action @{action_ref - "toggle-full-screen"}. + \<^bold>\<open>Workaround:\<close> Use native full-screen control of the macOS window manager. \<^item> \<^bold>\<open>Problem:\<close> Heap space of the JVM may fill up and render the Prover IDE unresponsive, e.g.\ when editing big Isabelle sessions with many theories.
--- a/src/Doc/ROOT Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Doc/ROOT Sun Jan 24 19:34:37 2021 +0100 @@ -229,7 +229,6 @@ "bibtex-mode.png" "build" "cite-completion.png" - "isabelle-jedit-hdpi.png" "isabelle-jedit.png" "markdown-document.png" "ml-debugger.png"
--- a/src/Doc/System/Environment.thy Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Doc/System/Environment.thy Sun Jan 24 19:34:37 2021 +0100 @@ -58,7 +58,7 @@ \<^enum> The file \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close> (if it exists) is run in the same way as the site default settings. Note that the variable @{setting ISABELLE_HOME_USER} has already been set before --- - usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2020\<close>. + usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2021\<close>. Thus individual users may override the site-wide defaults. Typically, a user settings file contains only a few lines, with some assignments that @@ -148,7 +148,7 @@ of the @{executable isabelle} executable. \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020\<close>''. + Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021\<close>''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
--- a/src/Doc/System/Misc.thy Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Doc/System/Misc.thy Sun Jan 24 19:34:37 2021 +0100 @@ -71,7 +71,7 @@ Isabelle installation: it needs to be a suitable version of Ubuntu Linux. The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For - Isabelle2020 this should be Ubuntu 18.04 LTS. + Isabelle2021 this should be Ubuntu 20.04 LTS. Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution. @@ -98,45 +98,49 @@ Produce a Dockerfile (without image) from a remote Isabelle distribution: @{verbatim [display] \<open> isabelle build_docker -E -n -o Dockerfile - https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020_linux.tar.gz\<close>} + https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz\<close>} Build a standard Isabelle Docker image from a local Isabelle distribution, with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point: @{verbatim [display] -\<open> isabelle build_docker -E -t test/isabelle:Isabelle2020 Isabelle2020_linux.tar.gz\<close>} +\<open> isabelle build_docker -E -t test/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz\<close>} Invoke the raw Isabelle/ML process within that image: @{verbatim [display] -\<open> docker run test/isabelle:Isabelle2020 process -e "Session.welcome ()"\<close>} +\<open> docker run test/isabelle:Isabelle2021 process -e "Session.welcome ()"\<close>} Invoke a Linux command-line tool within the contained Isabelle system environment: @{verbatim [display] -\<open> docker run test/isabelle:Isabelle2020 env uname -a\<close>} +\<open> docker run test/isabelle:Isabelle2021 env uname -a\<close>} The latter should always report a Linux operating system, even when running on Windows or macOS. \<close> -section \<open>Resolving Isabelle components \label{sec:tool-components}\<close> +section \<open>Managing Isabelle components \label{sec:tool-components}\<close> text \<open> - The @{tool_def components} tool resolves Isabelle components: + The @{tool_def components} tool manages Isabelle components: @{verbatim [display] \<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...] Options are: -I init user settings - -R URL component repository - (default $ISABELLE_COMPONENT_REPOSITORY) + -R URL component repository (default $ISABELLE_COMPONENT_REPOSITORY) -a resolve all missing components -l list status + -u DIR update $ISABELLE_HOME_USER/components: add directory + -x DIR update $ISABELLE_HOME_USER/components: remove directory - Resolve Isabelle components via download and installation. - COMPONENTS are identified via base name. + Resolve Isabelle components via download and installation: given COMPONENTS + are identified via base name. Further operations manage etc/settings and + etc/components in $ISABELLE_HOME_USER. - ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"\<close>} + ISABELLE_COMPONENT_REPOSITORY="..." + ISABELLE_HOME_USER="..." +\<close>} Components are initialized as described in \secref{sec:components} in a permissive manner, which can mark components as ``missing''. This state is @@ -153,13 +157,20 @@ installation takes place in the location that was specified in the attempt to initialize the component before. + \<^medskip> Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components with their location (full name) within the file-system. + \<^medskip> Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard components specified in the Isabelle repository clone --- this does not make any sense for regular Isabelle releases. If the file already exists, it needs to be edited manually according to the printed explanation. + + \<^medskip> + Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in + \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoid manual editing if + Isabelle configuration files. \<close> @@ -357,7 +368,7 @@ \<^medskip> The default is to output the full version string of the Isabelle - distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020: April 2020\<close>. + distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021: February 2021\<close>. The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial id of the @{setting ISABELLE_HOME} directory.
--- a/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 21 18:18:19 2021 +0100 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy Sun Jan 24 19:34:37 2021 +0100 @@ -77,8 +77,9 @@ then have 0: "Partial_order I" by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def trans_def I_def elim: trans_init_seg_of) - { fix R assume "R \<in> Chains I" - then have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast + have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)" if "R \<in> Chains I" for R + proof - + from that have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast have subch: "chain\<^sub>\<subseteq> R" using \<open>R \<in> Chains I\<close> I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def) have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" and @@ -106,10 +107,10 @@ by (rule downset_on_Union [OF \<open>\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p\<close>]) moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p" by (rule chain_subset_extension_on_Union [OF subch \<open>\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p\<close>]) - ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)" + ultimately show ?thesis using mono_Chains [OF I_init] and \<open>R \<in> Chains I\<close> by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) - } + qed then have 1: "\<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" if "R\<in>Chains I" for R using that by (subst FI) blast txt \<open>Zorn's Lemma yields a maximal wellorder m.\<close> @@ -196,8 +197,6 @@ where "p \<subseteq> r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}" from \<open>p \<subseteq> r\<close> have "p \<subseteq> ?r" using \<open>Field p \<subseteq> A\<close> by (auto simp: Field_def) - have 1: "Field ?r = A" using wo univ - by (fastforce simp: Field_def order_on_defs refl_on_def) have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" using \<open>Well_order r\<close> by (simp_all add: order_on_defs) have "refl_on A ?r" using \<open>Refl r\<close> by (auto simp: refl_on_def univ)
--- a/src/Pure/Admin/build_history.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Admin/build_history.scala Sun Jan 24 19:34:37 2021 +0100 @@ -7,11 +7,6 @@ package isabelle -import java.io.{File => JFile} -import java.time.format.DateTimeFormatter -import java.util.Locale - - object Build_History { /* log files */
--- a/src/Pure/Admin/build_release.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Admin/build_release.scala Sun Jan 24 19:34:37 2021 +0100 @@ -287,6 +287,8 @@ declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) +"$ISABELLE_HOME/lib/scripts/java-gui-setup" + exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \ @@ -310,7 +312,7 @@ <key>CFBundleIconFile</key> <string>isabelle.icns</string> <key>CFBundleIdentifier</key> -<string>de.tum.in.isabelle.""" + isabelle_name + """</string> +<string>de.tum.in.isabelle</string> <key>CFBundleDisplayName</key> <string>""" + isabelle_name + """</string> <key>CFBundleInfoDictionaryVersion</key> @@ -320,11 +322,11 @@ <key>CFBundlePackageType</key> <string>APPL</string> <key>CFBundleShortVersionString</key> -<string>""" + isabelle_rev + """</string> +<string>""" + isabelle_name + """</string> <key>CFBundleSignature</key> <string>????</string> <key>CFBundleVersion</key> -<string>1</string> +<string>""" + isabelle_rev + """</string> <key>NSHumanReadableCopyright</key> <string></string> <key>LSMinimumSystemVersion</key>
--- a/src/Pure/Admin/components.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Admin/components.scala Sun Jan 24 19:34:37 2021 +0100 @@ -130,6 +130,55 @@ File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) + /** manage user components **/ + + val components_path = Path.explode("$ISABELLE_HOME_USER/etc/components") + + def read_components(): List[String] = + if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) + else Nil + + def write_components(lines: List[String]): Unit = + { + Isabelle_System.make_directory(components_path.dir) + File.write(components_path, Library.terminate_lines(lines)) + } + + def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = + { + val path = path0.expand.absolute + if (!(path + Path.explode("etc/settings")).is_file && + !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path) + + val lines1 = read_components() + val lines2 = + lines1.filter(line => + line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) + val lines3 = if (add) lines2 ::: List(path.implode) else lines2 + + if (lines1 != lines3) write_components(lines3) + + val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" + progress.echo(prefix + " component " + path) + } + + + /* main entry point */ + + def main(args: Array[String]): Unit = + { + Command_Line.tool { + for (arg <- args) { + val add = + if (arg.startsWith("+")) true + else if (arg.startsWith("-")) false + else error("Bad argument: " + quote(arg)) + val path = Path.explode(arg.substring(1)) + update_components(add, path, progress = new Console_Progress) + } + } + } + /** build and publish components **/
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Jan 24 19:34:37 2021 +0100 @@ -10,7 +10,6 @@ import java.nio.file.Files import scala.annotation.tailrec -import scala.collection.mutable object Isabelle_Cronjob
--- a/src/Pure/General/symbol.ML Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/General/symbol.ML Sun Jan 24 19:34:37 2021 +0100 @@ -59,6 +59,7 @@ val is_quasi: symbol -> bool val is_blank: symbol -> bool val is_block_ctrl: symbol -> bool + val has_block_ctrl: symbol list -> bool val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool val beginning: int -> symbol list -> string @@ -408,6 +409,7 @@ fun is_blank s = kind s = Blank; val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"]; +val has_block_ctrl = exists is_block_ctrl; fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end; fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
--- a/src/Pure/Syntax/lexicon.ML Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Syntax/lexicon.ML Sun Jan 24 19:34:37 2021 +0100 @@ -40,8 +40,10 @@ val terminals: string list val is_terminal: string -> bool val get_terminal: string -> token option - val literal_markup: string -> Markup.T - val report_of_token: token -> Position.report + val suppress_literal_markup: string -> bool + val suppress_markup: token -> bool + val literal_markup: string -> Markup.T list + val reports_of_token: token -> Position.report list val reported_token_range: Proof.context -> token -> string val valued_token: token -> bool val implode_string: Symbol.symbol list -> string @@ -197,28 +199,35 @@ (* markup *) +val suppress_literal_markup = Symbol.has_block_ctrl o Symbol.explode; +fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok); + fun literal_markup s = - if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s) - then Markup.literal - else Markup.delimiter; + let val syms = Symbol.explode s in + if Symbol.has_block_ctrl syms then [] + else if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter syms + then [Markup.literal] + else [Markup.delimiter] + end; val token_kind_markup = - fn Type_Ident => Markup.tfree - | Type_Var => Markup.tvar - | Num => Markup.numeral - | Float => Markup.numeral - | Str => Markup.inner_string - | String => Markup.inner_string - | Cartouche => Markup.inner_cartouche - | Comment _ => Markup.comment1 - | _ => Markup.empty; + fn Type_Ident => [Markup.tfree] + | Type_Var => [Markup.tvar] + | Num => [Markup.numeral] + | Float => [Markup.numeral] + | Str => [Markup.inner_string] + | String => [Markup.inner_string] + | Cartouche => [Markup.inner_cartouche] + | Comment _ => [Markup.comment1] + | _ => []; -fun report_of_token tok = +fun reports_of_token tok = let - val markup = + val pos = pos_of_token tok; + val markups = if is_literal tok then literal_markup (str_of_token tok) else token_kind_markup (kind_of_token tok); - in (pos_of_token tok, markup) end; + in map (pair pos) markups end; fun reported_token_range ctxt tok = if is_proper tok
--- a/src/Pure/Syntax/printer.ML Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Syntax/printer.ML Sun Jan 24 19:34:37 2021 +0100 @@ -138,7 +138,7 @@ (if Lexicon.is_terminal s then 1000 else p); fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) = - apfst (cons (String (not (exists Symbol.is_block_ctrl (Symbol.explode s)), s))) + apfst (cons (String (not (Lexicon.suppress_literal_markup s), s))) (xsyms_to_syms xsyms) | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) = apfst (cons (arg s_p)) (xsyms_to_syms xsyms) @@ -232,7 +232,7 @@ val (Ts, args') = synT m (symbs, args); val T = if do_mark - then Pretty.marks_str (m @ [Lexicon.literal_markup s], s) + then Pretty.marks_str (m @ Lexicon.literal_markup s, s) else Pretty.str s; in (T :: Ts, args') end | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
--- a/src/Pure/Syntax/syntax_phases.ML Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Sun Jan 24 19:34:37 2021 +0100 @@ -158,6 +158,10 @@ fun report pos = Position.store_reports reports [pos]; val append_reports = Position.append_reports reports; + fun report_pos tok = + if Lexicon.suppress_markup tok then Position.none + else Lexicon.pos_of_token tok; + fun trans a args = (case trf a of NONE => Ast.mk_appl (Ast.Constant a) args @@ -169,7 +173,7 @@ else []; fun ast_of_position tok = - Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok)); + Ast.Variable (Term_Position.encode (report_pos tok)); fun ast_of_dummy a tok = Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok]; @@ -179,13 +183,13 @@ and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = let - val pos = Lexicon.pos_of_token tok; + val pos = report_pos tok; val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos); val _ = append_reports rs; in [Ast.Constant (Lexicon.mark_class c)] end | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = let - val pos = Lexicon.pos_of_token tok; + val pos = report_pos tok; val (Type (c, _), rs) = Proof_Context.check_type_name {proper = true, strict = false} ctxt (Lexicon.str_of_token tok, pos); @@ -204,7 +208,7 @@ val _ = pts |> List.app (fn Parser.Node _ => () | Parser.Tip tok => if Lexicon.valued_token tok then () - else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a); + else report (report_pos tok) (markup_entity ctxt) a); in [trans a (maps asts_of pts)] end | asts_of (Parser.Tip tok) = asts_of_token tok @@ -340,7 +344,7 @@ val ast_tr = Syntax.parse_ast_translation syn; val toks = Syntax.tokenize syn raw syms; - val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks); + val _ = Context_Position.reports ctxt (maps Lexicon.reports_of_token toks); val pts = Syntax.parse syn root (filter Lexicon.is_proper toks) handle ERROR msg =>
--- a/src/Pure/System/java_statistics.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/System/java_statistics.scala Sun Jan 24 19:34:37 2021 +0100 @@ -21,8 +21,8 @@ def memory_status(): Memory_Status = { val heap_size = Runtime.getRuntime.totalMemory() - val heap_used = heap_size - Runtime.getRuntime.freeMemory() - Memory_Status(heap_size, heap_used) + val heap_free = Runtime.getRuntime.freeMemory() + Memory_Status(heap_size, heap_free) }
--- a/src/Pure/System/options.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/System/options.scala Sun Jan 24 19:34:37 2021 +0100 @@ -120,7 +120,7 @@ case bad => error(bad.toString) } try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } } - catch { case ERROR(msg) => error(msg + Position.File(file_name)) } + catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) } } def parse_prefs(options: Options, content: String): Options =
--- a/src/Pure/Thy/bibtex.ML Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Thy/bibtex.ML Sun Jan 24 19:34:37 2021 +0100 @@ -46,17 +46,19 @@ (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position)) (fn ctxt => fn (opt, citations) => let - val thy = Proof_Context.theory_of ctxt; - val bibtex_entries = Resources.theory_bibtex_entries (Context.theory_long_name thy); val _ = - if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () + Context_Position.reports ctxt + (map (fn (name, pos) => (pos, Markup.citation name)) citations); + + val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt); + val bibtex_entries = Resources.theory_bibtex_entries thy_name; + val _ = + if null bibtex_entries andalso thy_name <> Context.PureN then () else citations |> List.app (fn (name, pos) => if member (op =) bibtex_entries name then () else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); - val _ = - Context_Position.reports ctxt - (map (fn (name, pos) => (pos, Markup.citation name)) citations); + val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]"); val arg = "{" ^ space_implode "," (map #1 citations) ^ "}"; in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
--- a/src/Pure/Tools/server.scala Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Pure/Tools/server.scala Sun Jan 24 19:34:37 2021 +0100 @@ -139,7 +139,7 @@ while (!finished) { Exn.capture(socket.accept) match { case Exn.Res(client) => - Isabelle_Thread.fork(name = "server_connection") { + Isabelle_Thread.fork(name = "client") { using(Connection(client))(connection => if (connection.read_password(password)) handle(connection)) }
--- a/src/Tools/Haskell/Haskell.thy Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Tools/Haskell/Haskell.thy Sun Jan 24 19:34:37 2021 +0100 @@ -67,7 +67,6 @@ space_explode, split_lines, trim_line, clean_name) where -import Data.Maybe import qualified Data.List as List import qualified Data.List.Split as Split import qualified Isabelle.Symbol as Symbol @@ -181,7 +180,6 @@ (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real) where -import Data.Maybe import qualified Data.List as List import qualified Text.Read as Read @@ -307,6 +305,8 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/markup.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} + module Isabelle.Markup ( T, empty, is_empty, properties, @@ -759,7 +759,6 @@ module Isabelle.File (setup, read, write, append) where import Prelude hiding (read) -import System.IO (IO) import qualified System.IO as IO setup :: IO.Handle -> IO () @@ -791,11 +790,11 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} + module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) where -import qualified Data.List as List - import Isabelle.Library import qualified Isabelle.Properties as Properties import qualified Isabelle.Markup as Markup @@ -874,6 +873,8 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} + module Isabelle.XML.Encode ( A, T, V, P, @@ -965,6 +966,8 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/xml.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} + module Isabelle.XML.Decode ( A, T, V, P, @@ -974,8 +977,6 @@ ) where -import Data.List ((!!)) - import Isabelle.Library import qualified Isabelle.Value as Value import qualified Isabelle.Properties as Properties @@ -1078,6 +1079,8 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-} + module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, buffer_body, buffer, string_of_body, string_of, parse_body, parse) where @@ -1205,6 +1208,8 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} + module Isabelle.Pretty ( T, symbolic, formatted, unformatted, @@ -1416,7 +1421,6 @@ where import Isabelle.Library -import qualified Isabelle.XML as XML import Isabelle.XML.Encode import Isabelle.Term @@ -1457,11 +1461,12 @@ See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>. -} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} + module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term) where import Isabelle.Library -import qualified Isabelle.XML as XML import Isabelle.XML.Decode import Isabelle.Term @@ -1514,7 +1519,6 @@ where import Data.ByteString (ByteString) -import qualified Data.ByteString import Data.UUID (UUID) import qualified Data.UUID as UUID import Data.UUID.V4 (nextRandom) @@ -1564,11 +1568,14 @@ and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>. -} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} + module Isabelle.Byte_Message ( write, write_line, read, read_block, trim_line, read_line, make_message, write_message, read_message, - make_line_message, write_line_message, read_line_message + make_line_message, write_line_message, read_line_message, + read_yxml, write_yxml ) where @@ -1577,11 +1584,10 @@ import Data.ByteString (ByteString) import qualified Data.ByteString as ByteString import qualified Data.ByteString.UTF8 as UTF8 -import Data.Word (Word8) - -import Control.Monad (when) +import qualified Isabelle.XML as XML +import qualified Isabelle.YXML as YXML + import Network.Socket (Socket) -import qualified Network.Socket as Socket import qualified Network.Socket.ByteString as ByteString import Isabelle.Library hiding (trim_line) @@ -1713,6 +1719,16 @@ case Value.parse_nat (UTF8.toString line) of Nothing -> return $ Just line Just n -> fmap trim_line . fst <$> read_block socket n + + +read_yxml :: Socket -> IO (Maybe XML.Body) +read_yxml socket = do + res <- read_line_message socket + return (YXML.parse_body . UTF8.toString <$> res) + +write_yxml :: Socket -> XML.Body -> IO () +write_yxml socket body = + write_line_message socket (UTF8.fromString (YXML.string_of_body body)) \<close> generate_file "Isabelle/Isabelle_Thread.hs" = \<open> @@ -1739,7 +1755,6 @@ where import Data.Unique -import Data.Maybe import Data.IORef import System.IO.Unsafe @@ -1747,7 +1762,6 @@ import Control.Monad (when, forM_) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map -import Control.Exception.Base (SomeException) import Control.Exception as Exception import Control.Concurrent (ThreadId) import qualified Control.Concurrent as Concurrent @@ -1898,7 +1912,7 @@ module Isabelle.Server ( localhost_name, localhost, publish_text, publish_stdout, - server + server, connection ) where @@ -1913,6 +1927,7 @@ import qualified Isabelle.UUID as UUID import qualified Isabelle.Byte_Message as Byte_Message import qualified Isabelle.Isabelle_Thread as Isabelle_Thread +import qualified Data.ByteString.UTF8 as UTF8 {- server address -} @@ -1963,6 +1978,32 @@ Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn Right () -> return ()) return () + + +{- client connection -} + +connection :: String -> String -> (Socket -> IO a) -> IO a +connection port password client = + Socket.withSocketsDo $ do + addr <- resolve + Exception.bracket (open addr) Socket.close body + where + resolve = do + let hints = + Socket.defaultHints { + Socket.addrFlags = [Socket.AI_NUMERICHOST, Socket.AI_NUMERICSERV], + Socket.addrSocketType = Socket.Stream } + head <$> Socket.getAddrInfo (Just hints) (Just "127.0.0.1") (Just port) + + open addr = do + socket <- Socket.socket (Socket.addrFamily addr) (Socket.addrSocketType addr) + (Socket.addrProtocol addr) + Socket.connect socket $ Socket.addrAddress addr + return socket + + body socket = do + Byte_Message.write_line socket (UTF8.fromString password) + client socket \<close> export_generated_files _
--- a/src/Tools/VSCode/extension/README.md Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Tools/VSCode/extension/README.md Sun Jan 24 19:34:37 2021 +0100 @@ -1,14 +1,15 @@ # Isabelle Prover IDE support This extension connects VSCode to the Isabelle Prover IDE infrastructure: it -requires a repository version of Isabelle. +requires Isabelle2021. The implementation is centered around the VSCode Language Server protocol, but with many add-ons that are specific to VSCode and Isabelle/PIDE. See also: - * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode> + * <https://isabelle.in.tum.de/website-Isabelle2021> + * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2021/src/Tools/VSCode> * <https://github.com/Microsoft/language-server-protocol> @@ -58,8 +59,8 @@ ### Isabelle/VSCode Installation - * Download a recent Isabelle development snapshot from - <https://isabelle.in.tum.de/devel/release_snapshot> + * Download Isabelle2021 from <https://isabelle.in.tum.de/website-Isabelle2021> + or any of its mirror sites. * Unpack and run the main Isabelle/jEdit application as usual, to ensure that the logic image is built properly and Isabelle works as expected. @@ -68,7 +69,7 @@ * Open the VSCode *Extensions* view and install the following: - + *Isabelle* (needs to fit to the underlying Isabelle release). + + *Isabelle2021* (needs to fit to the underlying Isabelle release). + *Prettify Symbols Mode* (important for display of Isabelle symbols). @@ -89,17 +90,17 @@ + Linux: ``` - "isabelle.home": "/home/makarius/Isabelle" + "isabelle.home": "/home/makarius/Isabelle2021" ``` + Mac OS X: ``` - "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle" + "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2021" ``` + Windows: ``` - "isabelle.home": "C:\\Users\\makarius\\Isabelle" + "isabelle.home": "C:\\Users\\makarius\\Isabelle2021" ``` * Restart the VSCode application to ensure that all extensions are properly
--- a/src/Tools/VSCode/extension/package.json Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Tools/VSCode/extension/package.json Sun Jan 24 19:34:37 2021 +0100 @@ -1,6 +1,6 @@ { - "name": "Isabelle", - "displayName": "Isabelle", + "name": "Isabelle2021", + "displayName": "Isabelle2021", "description": "Isabelle Prover IDE", "keywords": [ "theorem prover", @@ -10,7 +10,7 @@ "document preparation" ], "icon": "isabelle.png", - "version": "1.2.1", + "version": "1.2.2", "publisher": "makarius", "license": "MIT", "repository": { @@ -189,92 +189,350 @@ "default": "", "description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)." }, - "isabelle.unprocessed_light_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" }, - "isabelle.unprocessed_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" }, - "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" }, - "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.20)" }, - "isabelle.running_light_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" }, - "isabelle.running_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" }, - "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.40)" }, - "isabelle.running1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.40)" }, - "isabelle.canceled_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, - "isabelle.canceled_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, - "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, - "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, - "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.40)" }, - "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(204, 136, 0, 0.20)" }, - "isabelle.markdown_bullet1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" }, - "isabelle.markdown_bullet1_dark_color": { "type": "string", "default": "rgba(5, 199, 5, 0.20)" }, - "isabelle.markdown_bullet2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" }, - "isabelle.markdown_bullet2_dark_color": { "type": "string", "default": "rgba(204, 143, 0, 0.20)" }, - "isabelle.markdown_bullet3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" }, - "isabelle.markdown_bullet3_dark_color": { "type": "string", "default": "rgba(0, 0, 204, 0.20)" }, - "isabelle.markdown_bullet4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" }, - "isabelle.markdown_bullet4_dark_color": { "type": "string", "default": "rgba(204, 0, 105, 0.20)" }, - "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" }, - "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(150, 150, 150, 0.15)" }, - "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" }, - "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 214, 102, 0.15)" }, - "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" }, - "isabelle.writeln_dark_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" }, - "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }, - "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }, - "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, - "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, - "isabelle.error_light_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" }, - "isabelle.error_dark_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" }, - "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }, - "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" }, - "isabelle.main_light_color": { "type": "string", "default": "rgba(0, 0, 0, 1.00)" }, - "isabelle.main_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" }, - "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(175, 0, 219, 1.00)" }, - "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }, - "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" }, - "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" }, - "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(38, 127, 153, 1.00)" }, - "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(78, 201, 176), 1.00)" }, - "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, - "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, - "isabelle.improper_light_color": { "type": "string", "default": "rgba(205, 49, 49, 1.00)" }, - "isabelle.improper_dark_color": { "type": "string", "default": "rgba(244, 71, 71, 1.00)" }, - "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" }, - "isabelle.operator_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" }, - "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, - "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" }, - "isabelle.free_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" }, - "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.bound_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, - "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 16, 128, 1.00)" }, - "isabelle.var_dark_color": { "type": "string", "default": "rgba(156, 220, 254, 1.00)" }, - "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" }, - "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" }, - "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(163, 21, 21, 1.00)" }, - "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(206, 145, 120, 1.00)" }, - "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(129, 31, 63, 1.00)" }, - "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(209, 105, 105, 1.00)" }, - "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, - "isabelle.comment1_light_color": { "type": "string", "default": "rgba(129, 31, 63, 1.00)" }, - "isabelle.comment1_dark_color": { "type": "string", "default": "rgba(100, 102, 149, 1.00)" }, - "isabelle.comment2_light_color": { "type": "string", "default": "rgba(209, 105, 105, 1.00)" }, - "isabelle.comment2_dark_color": { "type": "string", "default": "rgba(206, 155, 120, 1.00)" }, - "isabelle.comment3_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.comment3_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, - "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(121, 94, 38, 1.00)" }, - "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(220, 220, 170, 1.00)" }, - "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, - "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }, - "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }, - "isabelle.raw_text_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }, - "isabelle.raw_text_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }, - "isabelle.plain_text_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }, - "isabelle.plain_text_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" } + "isabelle.unprocessed_light_color": { + "type": "string", + "default": "rgba(255, 160, 160, 1.00)" + }, + "isabelle.unprocessed_dark_color": { + "type": "string", + "default": "rgba(97, 0, 97, 1.00)" + }, + "isabelle.unprocessed1_light_color": { + "type": "string", + "default": "rgba(255, 160, 160, 0.20)" + }, + "isabelle.unprocessed1_dark_color": { + "type": "string", + "default": "rgba(97, 0, 97, 0.20)" + }, + "isabelle.running_light_color": { + "type": "string", + "default": "rgba(97, 0, 97, 1.00)" + }, + "isabelle.running_dark_color": { + "type": "string", + "default": "rgba(255, 160, 160, 1.00)" + }, + "isabelle.running1_light_color": { + "type": "string", + "default": "rgba(97, 0, 97, 0.40)" + }, + "isabelle.running1_dark_color": { + "type": "string", + "default": "rgba(255, 160, 160, 0.40)" + }, + "isabelle.canceled_light_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.canceled_dark_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.bad_light_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.bad_dark_color": { + "type": "string", + "default": "rgba(255, 106, 106, 0.40)" + }, + "isabelle.intensify_light_color": { + "type": "string", + "default": "rgba(255, 204, 102, 0.40)" + }, + "isabelle.intensify_dark_color": { + "type": "string", + "default": "rgba(204, 136, 0, 0.20)" + }, + "isabelle.markdown_bullet1_light_color": { + "type": "string", + "default": "rgba(218, 254, 218, 1.00)" + }, + "isabelle.markdown_bullet1_dark_color": { + "type": "string", + "default": "rgba(5, 199, 5, 0.20)" + }, + "isabelle.markdown_bullet2_light_color": { + "type": "string", + "default": "rgba(255, 240, 204, 1.00)" + }, + "isabelle.markdown_bullet2_dark_color": { + "type": "string", + "default": "rgba(204, 143, 0, 0.20)" + }, + "isabelle.markdown_bullet3_light_color": { + "type": "string", + "default": "rgba(231, 231, 255, 1.00)" + }, + "isabelle.markdown_bullet3_dark_color": { + "type": "string", + "default": "rgba(0, 0, 204, 0.20)" + }, + "isabelle.markdown_bullet4_light_color": { + "type": "string", + "default": "rgba(255, 224, 240, 1.00)" + }, + "isabelle.markdown_bullet4_dark_color": { + "type": "string", + "default": "rgba(204, 0, 105, 0.20)" + }, + "isabelle.quoted_light_color": { + "type": "string", + "default": "rgba(139, 139, 139, 0.10)" + }, + "isabelle.quoted_dark_color": { + "type": "string", + "default": "rgba(150, 150, 150, 0.15)" + }, + "isabelle.antiquoted_light_color": { + "type": "string", + "default": "rgba(255, 200, 50, 0.10)" + }, + "isabelle.antiquoted_dark_color": { + "type": "string", + "default": "rgba(255, 214, 102, 0.15)" + }, + "isabelle.writeln_light_color": { + "type": "string", + "default": "rgba(192, 192, 192, 1.0)" + }, + "isabelle.writeln_dark_color": { + "type": "string", + "default": "rgba(192, 192, 192, 1.0)" + }, + "isabelle.information_light_color": { + "type": "string", + "default": "rgba(193, 223, 238, 1.0)" + }, + "isabelle.information_dark_color": { + "type": "string", + "default": "rgba(193, 223, 238, 1.0)" + }, + "isabelle.warning_light_color": { + "type": "string", + "default": "rgba(255, 140, 0, 1.0)" + }, + "isabelle.warning_dark_color": { + "type": "string", + "default": "rgba(255, 140, 0, 1.0)" + }, + "isabelle.error_light_color": { + "type": "string", + "default": "rgba(178, 34, 34, 1.00)" + }, + "isabelle.error_dark_color": { + "type": "string", + "default": "rgba(178, 34, 34, 1.00)" + }, + "isabelle.spell_checker_light_color": { + "type": "string", + "default": "rgba(0, 0, 255, 1.0)" + }, + "isabelle.spell_checker_dark_color": { + "type": "string", + "default": "rgba(86, 156, 214, 1.00)" + }, + "isabelle.main_light_color": { + "type": "string", + "default": "rgba(0, 0, 0, 1.00)" + }, + "isabelle.main_dark_color": { + "type": "string", + "default": "rgba(212, 212, 212, 1.00)" + }, + "isabelle.keyword1_light_color": { + "type": "string", + "default": "rgba(175, 0, 219, 1.00)" + }, + "isabelle.keyword1_dark_color": { + "type": "string", + "default": "rgba(197, 134, 192, 1.00)" + }, + "isabelle.keyword2_light_color": { + "type": "string", + "default": "rgba(9, 136, 90, 1.00)" + }, + "isabelle.keyword2_dark_color": { + "type": "string", + "default": "rgba(181, 206, 168, 1.00)" + }, + "isabelle.keyword3_light_color": { + "type": "string", + "default": "rgba(38, 127, 153, 1.00)" + }, + "isabelle.keyword3_dark_color": { + "type": "string", + "default": "rgba(78, 201, 176), 1.00)" + }, + "isabelle.quasi_keyword_light_color": { + "type": "string", + "default": "rgba(153, 102, 255, 1.00)" + }, + "isabelle.quasi_keyword_dark_color": { + "type": "string", + "default": "rgba(153, 102, 255, 1.00)" + }, + "isabelle.improper_light_color": { + "type": "string", + "default": "rgba(205, 49, 49, 1.00)" + }, + "isabelle.improper_dark_color": { + "type": "string", + "default": "rgba(244, 71, 71, 1.00)" + }, + "isabelle.operator_light_color": { + "type": "string", + "default": "rgba(50, 50, 50, 1.00)" + }, + "isabelle.operator_dark_color": { + "type": "string", + "default": "rgba(212, 212, 212, 1.00)" + }, + "isabelle.tfree_light_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.tfree_dark_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.tvar_light_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.tvar_dark_color": { + "type": "string", + "default": "rgba(160, 32, 240, 1.00)" + }, + "isabelle.free_light_color": { + "type": "string", + "default": "rgba(0, 0, 255, 1.00)" + }, + "isabelle.free_dark_color": { + "type": "string", + "default": "rgba(86, 156, 214, 1.00)" + }, + "isabelle.skolem_light_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.skolem_dark_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.bound_light_color": { + "type": "string", + "default": "rgba(0, 128, 0, 1.00)" + }, + "isabelle.bound_dark_color": { + "type": "string", + "default": "rgba(96, 139, 78, 1.00)" + }, + "isabelle.var_light_color": { + "type": "string", + "default": "rgba(0, 16, 128, 1.00)" + }, + "isabelle.var_dark_color": { + "type": "string", + "default": "rgba(156, 220, 254, 1.00)" + }, + "isabelle.inner_numeral_light_color": { + "type": "string", + "default": "rgba(9, 136, 90, 1.00)" + }, + "isabelle.inner_numeral_dark_color": { + "type": "string", + "default": "rgba(181, 206, 168, 1.00)" + }, + "isabelle.inner_quoted_light_color": { + "type": "string", + "default": "rgba(163, 21, 21, 1.00)" + }, + "isabelle.inner_quoted_dark_color": { + "type": "string", + "default": "rgba(206, 145, 120, 1.00)" + }, + "isabelle.inner_cartouche_light_color": { + "type": "string", + "default": "rgba(129, 31, 63, 1.00)" + }, + "isabelle.inner_cartouche_dark_color": { + "type": "string", + "default": "rgba(209, 105, 105, 1.00)" + }, + "isabelle.inner_comment_light_color": { + "type": "string", + "default": "rgba(0, 128, 0, 1.00)" + }, + "isabelle.inner_comment_dark_color": { + "type": "string", + "default": "rgba(96, 139, 78, 1.00)" + }, + "isabelle.comment1_light_color": { + "type": "string", + "default": "rgba(129, 31, 63, 1.00)" + }, + "isabelle.comment1_dark_color": { + "type": "string", + "default": "rgba(100, 102, 149, 1.00)" + }, + "isabelle.comment2_light_color": { + "type": "string", + "default": "rgba(209, 105, 105, 1.00)" + }, + "isabelle.comment2_dark_color": { + "type": "string", + "default": "rgba(206, 155, 120, 1.00)" + }, + "isabelle.comment3_light_color": { + "type": "string", + "default": "rgba(0, 128, 0, 1.00)" + }, + "isabelle.comment3_dark_color": { + "type": "string", + "default": "rgba(96, 139, 78, 1.00)" + }, + "isabelle.dynamic_light_color": { + "type": "string", + "default": "rgba(121, 94, 38, 1.00)" + }, + "isabelle.dynamic_dark_color": { + "type": "string", + "default": "rgba(220, 220, 170, 1.00)" + }, + "isabelle.class_parameter_light_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.class_parameter_dark_color": { + "type": "string", + "default": "rgba(210, 105, 30, 1.00)" + }, + "isabelle.antiquote_light_color": { + "type": "string", + "default": "rgba(102, 0, 204, 1.00)" + }, + "isabelle.antiquote_dark_color": { + "type": "string", + "default": "rgba(197, 134, 192, 1.00)" + }, + "isabelle.raw_text_light_color": { + "type": "string", + "default": "rgba(102, 0, 204, 1.00)" + }, + "isabelle.raw_text_dark_color": { + "type": "string", + "default": "rgba(197, 134, 192, 1.00)" + }, + "isabelle.plain_text_light_color": { + "type": "string", + "default": "rgba(102, 0, 204, 1.00)" + }, + "isabelle.plain_text_dark_color": { + "type": "string", + "default": "rgba(197, 134, 192, 1.00)" + } } } }, @@ -285,9 +543,9 @@ }, "devDependencies": { "@types/mocha": "^2.2.48", - "@types/node": "^7.0.66", + "@types/node": "^7.10.14", "mocha": "^3.5.3", - "typescript": "^2.9.2", + "typescript": "^3.7.9", "vscode": "^1.1.36" }, "dependencies": {
--- a/src/Tools/VSCode/extension/src/symbol.ts Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Tools/VSCode/extension/src/symbol.ts Sun Jan 24 19:34:37 2021 +0100 @@ -122,7 +122,7 @@ if (prettify_symbols_mode) { prettify_symbols_mode.activate().then(() => { - const substitutions = [] as [Substitution] + const substitutions: Substitution[] = [] for (const entry of names) { const sym = entry[0] substitutions.push(
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Jan 24 19:34:37 2021 +0100 @@ -408,6 +408,8 @@ if [ "$BUILD_ONLY" = false ] then + "$ISABELLE_HOME/lib/scripts/java-gui-setup" + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
--- a/src/Tools/jEdit/src/jEdit.props Thu Jan 21 18:18:19 2021 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Sun Jan 24 19:34:37 2021 +0100 @@ -187,6 +187,7 @@ helpviewer.font=Isabelle DejaVu Serif helpviewer.fontsize=12 home.shortcut= +hypersearch-results.dock-position=right insert-newline-indent.shortcut= insert-newline.shortcut= isabelle-debugger.dock-position=floating