*** 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev