[isabelle-dev] NEWS: isabelle update

[Makarius]

*** System ***

* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
section "Theory update". Theory sessions are specified as in "isabelle
dump".


This refers to Isabelle/1d2d4ae9ab81 and there is some documentation in
the "system" manual as usual. The "isabelle update" tool is a corollary
of the "Headless PIDE" session; it opens new possibilities for
systematic maintenance of formal sources at a large scale. In the next
round I will provide options to replace old-style ASCII syntax, e.g. %
== ==> -->.

An example is Isabelle/a96320074298, which is the result of applying
"isabelle update -u path_cartouches" for all sessions.


So far I have refrained from too much updating, because I am not sure
how far we are in the process of mental adaption, to see cartouches
almost everywhere. In particular "isabelle update -u
inner_syntax_cartouches" will be quite significant:

  * Different visual appearance of Isabelle sources: potentially odd for
long-term users, but less odd for newcomers (i.e. no longer questions
like "What is the meaning of double-quotes around the logical language?"
at first-time exposure).

  * It potentially affects corner cases for implicit or explicit
double-quotes in document preparation (cf. options thy_output_quotes /
thy_output_source or @{term [quotes] "..."} / @{term [source] "..."}).

  * When inner syntax double-quotes are discontinued eventually, the
inner syntax of the HOL library may use double quotes for char/string
literals, instead of slightly odd double single-quotes.


Here is a reminder of the general approach and trend of recent years:

  * embedded languages normally use cartouches, while double quotes are
old-style / legacy;

  * names normally use plain identifiers, but double quotes are
available to escape conflicts with keywords.


	Makarius