provide naproche-20220917;

clarified NEWS;

proper platform directory x86_64-linux, to have it purged for other platforms; tuned README;

MLton component for x86_64-linux;

clarified Docker base image;

proper file headers;

tuned messages;

support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;

omit menu for unfinished tool;

include ssh + rsync as required for Isabelle tools, e.g. "isabelle sync";

more robust: snap version of docker cannot access /tmp;

tuned signature;

update to scala-3.2.0; enforce rebuild of Isabelle/ML + Isabelle/Scala;

avoid crash of JLine on Windows;

update to jdk-17.0.4.1+1 from 22-Aug-2022 (https://docs.azul.com/core/zulu-openjdk/release-notes/11.58-17.36-august-2022);

clarified default, following 8b695e59db3f;

tuned signature;

tuned;

clarified modules;

discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;

clarified options;

clarified options;

discontinued unclear timeout (stemming from jEdit JSch setup, see 14782d58a503), to make it work with native Windows ssh.exe;

proper time values in seconds;

clarified run_sftp: avoid platform_path via careful use of tmp_dir, to support both Windows and Cygwin ssh; discontinued run_scp: use run_sftp instead;

more robust, notably for macOS (see also ff92d6edff2c);

back to plain /tmp (despite 1df53737c59b): relevant for ssh on macOS, to avoid error "unix_listener: path too long for Unix domain socket";

tuned names;

proper order of platforms, to make it work uniformly on all plaform families;

more portable;

build both arm64-darwin and x86_64-darwin on Apple ARM hardware; tuned messages;

unused;

tuned message;

more items;

more robust: do not assume Bash syntax while testing for it;

obsolete;

merged

proper treatment of complex multi-line script;

more robust;

more robust: Bash.string operations require remote bash;

support port forwarding without multiplexing (for the sake of Windows);

misc tuning and clarification; proper shutdown_hook;

clarified signature;

clarified signature;

clarified signature;

More on division concerning gauss numbers.

more robust adhoc shell script: work with Isabelle_System.export_isabelle_identifier;

more concise instance-specific rules on euclidean relation

merged

Tidied a few more proofs

merged

tidied a few ugly proofs

let rsync re-use ssh connection via control path;

clarified command-line;

clarified command-line;

tuned signature;

proper port for Mercurial;

clarified default: do not override port from ssh_config, which could be different from 22;

proper Scala expression;

clarified signature: separate unrelated modules;

tuned;

obsolete;

obsolete;

clarified error;

merged

removed remains of proxy_host management: delegated to .ssh/config;

ssh client via regular OpenSSH tools, with authentic use of .ssh/config (notably proxy configuration); tuned signature;

putting together related theorems

dropped auxiliary lemma

unused;

clarified operation: avoid perl;

discontinued unused operations;

clarified signature: avoid exposure of JSch types;

clarified signature: discontinue somewhat pointless SSH.Context;

tuned;

proper path;

Added tag Isabelle2022-RC1 for changeset 6308eaaa88f1

clarified release packaging: naproche-20220910 lacks arm64-linux support (and crashes);

more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);

merged;

update for release;

more command-line options;

less specialized euclidean relation on int

update to Isabelle2022 and Ubuntu 22.04;

proper comment: Phabricator remains on Ubuntu 20.04, which is still required as build environment for old Mercurial 3.9.2 with Python 2;

more operations: for testing purposes;

provide naproche-20220910 (inactive);

clarified directory names (e.g. for multi-platform remote execution): avoid being deleted via isabelle.Components.purge;

unused;

update for release;

tuned: prefer Scala Regex operations;

tuning and updates for release;

NEWS;

discontinued somewhat pointless option: Proof_Display.pretty_goal_inst should always work smoothly (and not crash unexpectedly);

give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;

merged

discontinue fragile operations;

proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);

enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);

updated documentation;

support multiple sessions, with cumulative errors; tuned command usage;

support regex patterns on messages;

support Pretty.unformatted, similar to ML version;

removed odd TODO item (see 3391a493f39a);

tuned signature;

tuned output: more Pretty.item;

tuned signature;

clarified failure: warning for logical error, exception for program breakdown;

print goal instantiation for global qed (and variations);

clarified output;

more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);

clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);

updated to postgresql-42.5.0;

tool to build Isabelle component for PostgreSQL JDBC;

clarified goal structure with proper instantiation of main goal, to support "show_goal_inst";

option "show_states" for more verbosity of batch-builds;

tuned --- avoid warnings;

proper antiquotations;

inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;

proper antiquotations;