# HG changeset patch # User paulson # Date 1584905473 0 # Node ID 3904cfde1aa991a09c8a475da009d2b9ad6d798c # Parent 200ec7c4c1a55fa1fdd5f65dcf7bbe0975d2df3e# Parent e30dbfa53b0d59b16297232caa5cd11300bd2e73 merged diff -r e30dbfa53b0d -r 3904cfde1aa9 NEWS --- a/NEWS Sun Mar 22 19:02:39 2020 +0000 +++ b/NEWS Sun Mar 22 19:31:13 2020 +0000 @@ -94,6 +94,19 @@ automatic font scaling is usually absent on Linux, in contrast to Windows and macOS. +* The default value for the jEdit property "view.antiAlias" (menu item +Utilities / Global Options / Text Area / Anti Aliased smooth text) is +now "subpixel HRGB", instead of former "standard". Especially on Linux +this often leads to faster text rendering, but can also cause problems +with odd color shades. An alternative is to switch back to "standard" +here, and set the following Java system property: + + isabelle jedit -Dsun.java2d.opengl=true + +This can be made persistent via JEDIT_JAVA_OPTIONS in +$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop +application there is a corresponding options file in the same directory. + *** Isabelle/VSCode Prover IDE *** @@ -1488,6 +1501,9 @@ is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32, ISABELLE_PLATFORM64. +* The command-line tool "isabelle build_docker" has been slightly +improved: it is now properly documented in the "system" manual. + * Command-line tool "isabelle build_docker" builds a Docker image from the Isabelle application bundle for Linux. See also https://hub.docker.com/r/makarius/isabelle diff -r e30dbfa53b0d -r 3904cfde1aa9 README_REPOSITORY --- a/README_REPOSITORY Sun Mar 22 19:02:39 2020 +0000 +++ b/README_REPOSITORY Sun Mar 22 19:31:13 2020 +0000 @@ -34,8 +34,6 @@ ./bin/isabelle jedit -l HOL - ./bin/isabelle jedit -b -f #optional: force fresh build of Isabelle/Scala - 4. Access documentation (bash shell commands): ./bin/isabelle build_doc -a @@ -48,11 +46,9 @@ Mercurial https://www.mercurial-scm.org belongs to source code management systems that follow the so-called paradigm of "distributed -version control". This means plain revision control without the -legacy of CVS or SVN (and without the extra complexity introduced by -git). See also http://hginit.com/ for an introduction to the main -ideas. The Mercurial book http://hgbook.red-bean.com/ explains many -more details. +version control". This means plain versioning without the legacy of +SVN and the extra complexity of GIT. See also +https://www.mercurial-scm.org/learn Mercurial offers some flexibility in organizing the flow of changes, both between individual developers and designated pull/push areas that @@ -100,7 +96,7 @@ as follows: [ui] - username = XXX + username = ABC Isabelle contributors are free to choose either a short "login name" (for accounts at TU Munich) or a "full name" -- with or without mail @@ -136,8 +132,7 @@ quite easy to publish changed clones again on the web, using the ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts that are included in the Mercurial distribution, and send a "pull -request" to someone else. There are also public hosting services for -Mercurial repositories, notably Bitbucket. +request" to someone else. The downstream/upstream mode of operation is quite common in the distributed version control community, and works well for occasional diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/Isar_Ref/Generic.thy Sun Mar 22 19:31:13 2020 +0000 @@ -1301,8 +1301,8 @@ The rule \P \ P \ Q\ is unsafe because it reduces \P \ Q\ to \P\, which might turn out as premature choice of an - unprovable subgoal. Any rule is unsafe whose premises contain new - unknowns. The elimination rule \\x. P x \ (P t \ Q) \ Q\ is + unprovable subgoal. Any rule whose premises contain new unknowns is + unsafe. The elimination rule \\x. P x \ (P t \ Q) \ Q\ is unsafe, since it is applied via elim-resolution, which discards the assumption \\x. P x\ and replaces it by the weaker assumption \P t\. The rule \P t \ \x. P x\ is @@ -1316,8 +1316,8 @@ that \(\E)\ is unsafe, because repeated application of it could generate exponentially many subgoals. Induction rules are unsafe because inductive proofs are difficult to set up - automatically. Any inference is unsafe that instantiates an unknown - in the proof state --- thus matching must be used, rather than + automatically. Any inference that instantiates an unknown + in the proof state is unsafe --- thus matching must be used, rather than unification. Even proof by assumption is unsafe if it instantiates unknowns shared with other subgoals. diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sun Mar 22 19:31:13 2020 +0000 @@ -2434,7 +2434,7 @@ Variant \code nbe\ accepts also non-left-linear equations for \<^emph>\normalization by evaluation\ only. - Variants \code drop:\ and \code abort:\ take a list of constant as arguments + Variants \code drop:\ and \code abort:\ take a list of constants as arguments and drop all code equations declared for them. In the case of \abort\, these constants then do not require to a specification by means of code equations; if needed these are implemented by program abort (exception) diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/Isar_Ref/Proof.thy Sun Mar 22 19:31:13 2020 +0000 @@ -1190,10 +1190,10 @@ declared using the @{attribute_def induct_simp} attribute. The optional ``\arbitrary: x\<^sub>1 \ x\<^sub>m\'' specification generalizes variables - \x\<^sub>1, \, x\<^sub>m\ of the original goal before applying induction. One can - separate variables by ``\and\'' to generalize them in other goals then the - first. Thus induction hypotheses may become sufficiently general to get the - proof through. Together with definitional instantiations, one may + \x\<^sub>1, \, x\<^sub>m\ of the original goal before applying induction. It is possible + to separate variables by ``\and\'' to generalize in goals other than + the first. Thus induction hypotheses may become sufficiently general to get + the proof through. Together with definitional instantiations, one may effectively perform induction over expressions of a certain structure. The optional ``\taking: t\<^sub>1 \ t\<^sub>n\'' specification provides additional diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/Isar_Ref/Spec.thy Sun Mar 22 19:31:13 2020 +0000 @@ -194,7 +194,7 @@ arguments; a syntactic abbreviation links the long form with the abstract version of the target context. For example, \a \ t[x]\ becomes \c.a ?x \ t[?x]\ at the theory level (for arbitrary \?x\), together with a local - abbreviation \c \ c.a x\ in the target context (for the fixed parameter + abbreviation \a \ c.a x\ in the target context (for the fixed parameter \x\). Theorems are exported by discharging the assumptions and generalizing the @@ -365,7 +365,7 @@ \<^descr> \<^theory_text>\axiomatization c\<^sub>1 \ c\<^sub>m where \\<^sub>1 \ \\<^sub>n\ introduces several constants simultaneously and states axiomatic properties for these. The constants are marked as being specified once and for all, which prevents additional - specifications for the same constants later on, but it is always possible do + specifications for the same constants later on, but it is always possible to emit axiomatizations without referring to particular constants. Note that lack of precise dependency tracking of axiomatizations may disrupt the well-formedness of an otherwise definitional theory. @@ -542,7 +542,7 @@ expressions automatically takes care of the most general typing that the combined context elements may acquire. - The \import\ consists of a locale expression; see \secref{sec:proof-context} + The \import\ consists of a locale expression; see \secref{sec:locale-expr} above. Its \<^theory_text>\for\ clause defines the parameters of \import\. These are parameters of the defined locale. Locale parameters whose instantiation is omitted automatically extend the (possibly empty) \<^theory_text>\for\ clause: they are @@ -949,7 +949,7 @@ \<^medskip> Co-regularity is a very fundamental property of the order-sorted algebra of - types. For example, it entails principle types and most general unifiers, + types. For example, it entails principal types and most general unifiers, e.g.\ see @{cite "nipkow-prehofer"}. \ diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/JEdit/JEdit.thy Sun Mar 22 19:31:13 2020 +0000 @@ -305,7 +305,7 @@ The \<^verbatim>\-n\ option reports the server name, and the \<^verbatim>\-s\ option provides a different server name. The default server name is the official distribution - name (e.g.\ \<^verbatim>\Isabelle2019\). Thus @{tool jedit_client} can connect to the + name (e.g.\ \<^verbatim>\Isabelle2020\). Thus @{tool jedit_client} can connect to the Isabelle desktop application without further options. The \<^verbatim>\-p\ option allows to override the implicit default of the system @@ -2194,6 +2194,24 @@ \<^bold>\Workaround:\ Use action @{action isabelle.draft} and print via the Web browser. + \<^item> \<^bold>\Problem:\ Antialiased text rendering may show bad performance or bad + visual quality, notably on Linux/X11. + + \<^bold>\Workaround:\ The property \<^verbatim>\view.antiAlias\ (via menu item Utilities / + Global Options / Text Area / Anti Aliased smooth text) has the main impact + on text rendering, but some related properties may also change the + behaviour. The default is \<^verbatim>\view.antiAlias=subpixel HRGB\: it can be much + faster than \<^verbatim>\standard\, but occasionally causes problems with odd color + shades. An alternative is to have \<^verbatim>\view.antiAlias=standard\ and set a Java + system property like this:\<^footnote>\See also + \<^url>\https://docs.oracle.com/javase/10/troubleshoot/java-2d-pipeline-rendering-and-properties.htm\.\ + @{verbatim [display] \isabelle jedit -Dsun.java2d.opengl=true\} + + If this works reliably, it can be made persistent via @{setting + JEDIT_JAVA_OPTIONS} within \<^path>\$ISABELLE_HOME_USER/etc/settings\. For + the Isabelle desktop ``app'', there is a corresponding file with Java + runtime options in the main directory (name depends on the OS platform). + \<^item> \<^bold>\Problem:\ Some Linux/X11 input methods such as IBus tend to disrupt key event handling of Java/AWT/Swing. diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/System/Environment.thy Sun Mar 22 19:31:13 2020 +0000 @@ -58,7 +58,7 @@ \<^enum> The file \<^path>\$ISABELLE_HOME_USER/etc/settings\ (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>\$USER_HOME/.isabelle/Isabelle2018\. + usually to something like \<^verbatim>\$USER_HOME/.isabelle/Isabelle2020\. 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}\\<^sup>*\] refers to the name of this - Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2018\''. + Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2020\''. \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\\<^sup>*\] diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/System/Misc.thy Sun Mar 22 19:31:13 2020 +0000 @@ -11,6 +11,113 @@ alphabetical order. \ +section \Building Isabelle docker images\ + +text \ + Docker\<^footnote>\\<^url>\https://docs.docker.com\\ provides a self-contained environment + for complex applications called \<^emph>\container\, although it does not fully + contain the program in a strict sense of the word. This includes basic + operating system services (usually based on Linux), shared libraries and + other required packages. Thus Docker is a light-weight alternative to + regular virtual machines, or a heavy-weight alternative to conventional + self-contained applications. + + Although Isabelle can be easily run on a variety of OS environments without + extra containment, Docker images may occasionally be useful when a + standardized Linux environment is required, even on + Windows\<^footnote>\\<^url>\https://docs.docker.com/docker-for-windows\\ and + macOS\<^footnote>\\<^url>\https://docs.docker.com/docker-for-mac\\. Further uses are in + common cloud computing environments, where applications need to be submitted + as Docker images in the first place. + + \<^medskip> + The @{tool_def build_docker} tool builds docker images from a standard + Isabelle application archive for Linux: + + @{verbatim [display] +\Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE + + Options are: + -B NAME base image (default "ubuntu") + -E set bin/isabelle as entrypoint + -P NAME additional Ubuntu package collection ("X11", "latex") + -l NAME default logic (default ISABELLE_LOGIC="HOL") + -n no docker build + -o FILE output generated Dockerfile + -p NAME additional Ubuntu package + -t TAG docker build tag + -v verbose + + Build Isabelle docker image with default logic image, using a standard + Isabelle application archive for Linux (local file or remote URL).\} + + Option \<^verbatim>\-E\ sets \<^verbatim>\bin/isabelle\ of the contained Isabelle distribution as + the standard entry point of the Docker image. Thus \<^verbatim>\docker run\ will + imitate the \<^verbatim>\isabelle\ command-line tool (\secref{sec:isabelle-tool}) of a + regular local installation, but it lacks proper GUI support: \<^verbatim>\isabelle jedit\ + will not work without further provisions. Note that the default entrypoint + may be changed later via \<^verbatim>\docker run --entrypoint="..."\. + + Option \<^verbatim>\-t\ specifies the Docker image tag: this a symbolic name within the + local Docker name space, but also relevant for Docker + Hub\<^footnote>\\<^url>\https://hub.docker.com\\. + + Option \<^verbatim>\-l\ specifies the default logic image of the Isabelle distribution + contained in the Docker environment: it will be produced by \<^verbatim>\isabelle build -b\ + as usual (\secref{sec:tool-build}) and stored within the image. + + \<^medskip> + Option \<^verbatim>\-B\ specifies the Docker image taken as starting point for the + Isabelle installation: it needs to be a suitable version of Ubuntu Linux. + The default \<^verbatim>\ubuntu\ refers to the latest LTS version provided by Canonical + as the official Ubuntu vendor\<^footnote>\\<^url>\https://hub.docker.com/_/ubuntu\\. For + Isabelle2020 this should be Ubuntu 18.04 LTS. + + Option \<^verbatim>\-p\ includes additional Ubuntu packages, using the terminology + of \<^verbatim>\apt-get install\ within the underlying Linux distribution. + + Option \<^verbatim>\-P\ refers to high-level package collections: \<^verbatim>\X11\ or \<^verbatim>\latex\ as + provided by \<^verbatim>\isabelle build_docker\ (assuming Ubuntu 18.04 LTS). This + imposes extra weight on the resulting Docker images. Note that \<^verbatim>\X11\ will + only provide remote X11 support according to the modest GUI quality + standards of the late 1990-ies. + + \<^medskip> + Option \<^verbatim>\-n\ suppresses the actual \<^verbatim>\docker build\ process. Option \<^verbatim>\-o\ + outputs the generated \<^verbatim>\Dockerfile\. Both options together produce a + Dockerfile only, which might be useful for informative purposes or other + tools. + + Option \<^verbatim>\-v\ disables quiet-mode of the underlying \<^verbatim>\docker build\ process. +\ + + +subsubsection \Examples\ + +text \ + Produce a Dockerfile (without image) from a remote Isabelle distribution: + @{verbatim [display] +\ isabelle build_docker -E -n -o Dockerfile + https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020_linux.tar.gz\} + + Build a standard Isabelle Docker image from a local Isabelle distribution, + with \<^verbatim>\bin/isabelle\ as executable entry point: + + @{verbatim [display] +\ isabelle build_docker -E -t test/isabelle:Isabelle2020 Isabelle2020_linux.tar.gz\} + + Invoke the raw Isabelle/ML process within that image: + @{verbatim [display] +\ docker run test/isabelle:Isabelle2020 process -e "Session.welcome ()"\} + + Invoke a Linux command-line tool within the contained Isabelle system + environment: + @{verbatim [display] +\ docker run test/isabelle:Isabelle2020 env uname -a\} + The latter should always report a Linux operating system, even when running + on Windows or macOS. +\ + section \Resolving Isabelle components \label{sec:tool-components}\ @@ -267,7 +374,7 @@ \<^medskip> The default is to output the full version string of the Isabelle - distribution, e.g.\ ``\<^verbatim>\Isabelle2018: August 2018\. + distribution, e.g.\ ``\<^verbatim>\Isabelle2020: April 2020\. The \<^verbatim>\-i\ option produces a short identification derived from the Mercurial id of the @{setting ISABELLE_HOME} directory. diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Doc/manual.bib --- a/src/Doc/manual.bib Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Doc/manual.bib Sun Mar 22 19:31:13 2020 +0000 @@ -2204,8 +2204,8 @@ booktitle = {Intelligent Computer Mathematics (CICM 2019)}, year = {2019}, editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Sacerdoti Coen, Claudio}, - volume = {????}, - series = LNAI, + volume = {11617}, + series = "LNAI", publisher = {Springer}, note = {\url{https://arxiv.org/abs/1905.01735}} } diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/PIDE/rendering.scala Sun Mar 22 19:31:13 2020 +0000 @@ -209,7 +209,7 @@ Markup.BAD) val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY) - val error_elements = Markup.Elements(Markup.ERROR, Markup.BAD) + val error_elements = Markup.Elements(Markup.ERROR) val caret_focus_elements = Markup.Elements(Markup.ENTITY) diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/System/isabelle_system.scala Sun Mar 22 19:31:13 2020 +0000 @@ -170,7 +170,7 @@ /* tmp files */ - private def isabelle_tmp_prefix(): JFile = + def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/Thy/sessions.scala Sun Mar 22 19:31:13 2020 +0000 @@ -222,7 +222,7 @@ val required_sessions = dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) .map(theory => imports_base.theory_qualifier(theory)) - .filterNot(_ == info.name) + .filter(name => name != info.name && sessions_structure.defined(name)) val required_subgraph = sessions_structure.imports_graph @@ -386,6 +386,8 @@ if (required_theories.isEmpty) (ancestor.get, Nil) else { val other_name = info.name + "_requirements(" + ancestor.get + ")" + Isabelle_System.isabelle_tmp_prefix() + (other_name, List( make_info(info.options, diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/Tools/build.scala Sun Mar 22 19:31:13 2020 +0000 @@ -294,7 +294,6 @@ } process.result( - progress_stderr = Output.writeln(_), progress_stdout = (line: String) => Library.try_unprefix("\floading_theory = ", line) match { case Some(theory) => diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/Tools/build_docker.scala --- a/src/Pure/Tools/build_docker.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/Tools/build_docker.scala Sun Mar 22 19:31:13 2020 +0000 @@ -67,7 +67,8 @@ mv """ + isabelle_name + """ Isabelle && \ perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \ perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \ - Isabelle/bin/isabelle build -o system_heaps -b """ + logic + + Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \ + rm Isabelle.tar.gz""" + (if (entrypoint) """ ENTRYPOINT ["Isabelle/bin/isabelle"] @@ -128,13 +129,6 @@ Build Isabelle docker image with default logic image, using a standard Isabelle application archive for Linux (local file or remote URL). - - Examples: - - isabelle build_docker -E -t test/isabelle:Isabelle2019 Isabelle2019_linux.tar.gz - - isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2019_linux.tar.gz - """, "B:" -> (arg => base = arg), "E" -> (_ => entrypoint = true), diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/Tools/dump.scala Sun Mar 22 19:31:13 2020 +0000 @@ -98,7 +98,8 @@ dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, - pure_base: Boolean = false): Context = + pure_base: Boolean = false, + skip_base: Boolean = false): Context = { val session_options: Options = { @@ -125,7 +126,7 @@ val deps: Sessions.Deps = Sessions.deps(sessions_structure, progress = progress).check_errors - new Context(options, progress, dirs, select_dirs, pure_base, session_options, deps) + new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps) } } @@ -135,6 +136,7 @@ val dirs: List[Path], val select_dirs: List[Path], val pure_base: Boolean, + val skip_base: Boolean, val session_options: Options, val deps: Sessions.Deps) { @@ -189,7 +191,7 @@ val PURE = isabelle.Thy_Header.PURE val base = - if (logic == PURE && !pure_base) Nil + if ((logic == PURE && !pure_base) || skip_base) Nil else make_session(base_sessions, session_logic = PURE, strict = logic == PURE) val main = diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/Tools/update.scala Sun Mar 22 19:31:13 2020 +0000 @@ -18,7 +18,7 @@ { val context = Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs, - selection = selection) + selection = selection, skip_base = true) context.build_logic(logic) diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Pure/thm_deps.ML Sun Mar 22 19:31:13 2020 +0000 @@ -42,7 +42,11 @@ fun prt_oracle (ora, NONE) = prt_ora ora | prt_oracle (ora, SOME prop) = prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop]; - in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; + val oracles = + (case try all_oracles thms of + SOME oracles => oracles + | NONE => error "Malformed proofs") + in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end; (* thm_deps *) @@ -70,8 +74,12 @@ fun pretty_thm_deps thy thms = let val ctxt = Proof_Context.init_global thy; + val deps = + (case try (thm_deps thy) thms of + SOME deps => deps + | NONE => error "Malformed proofs"); val items = - map #2 (thm_deps thy thms) + map #2 deps |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i)) |> sort_by (#2 o #1) |> map (fn ((marks, xname), i) => diff -r e30dbfa53b0d -r 3904cfde1aa9 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Sun Mar 22 19:02:39 2020 +0000 +++ b/src/Tools/jEdit/src/jEdit.props Sun Mar 22 19:31:13 2020 +0000 @@ -321,7 +321,7 @@ vfs.favorite.4=isabelle-export: vfs.favorite.5.type=1 vfs.favorite.5=isabelle-session: -view.antiAlias=standard +view.antiAlias=subpixel HRGB view.blockCaret=true view.caretBlink=false view.docking.framework=PIDE diff -r e30dbfa53b0d -r 3904cfde1aa9 src/ZF/Constructible/AC_in_L.thy --- a/src/ZF/Constructible/AC_in_L.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/ZF/Constructible/AC_in_L.thy Sun Mar 22 19:31:13 2020 +0000 @@ -460,7 +460,7 @@ apply (blast dest!: well_ord_L_r intro: well_ord_subset) done -interpretation L?: M_basic L by (rule M_basic_L) +interpretation L: M_basic L by (rule M_basic_L) theorem "\x[L]. \r. wellordered(L,x,r)" proof @@ -469,7 +469,7 @@ then obtain r where "well_ord(x,r)" by (blast dest: L_implies_AC) thus "\r. wellordered(L,x,r)" - by (blast intro: well_ord_imp_relativized) + by (blast intro: L.well_ord_imp_relativized) qed text\In order to prove \<^term>\ \r[L]. wellordered(L,x,r)\, it's necessary to know diff -r e30dbfa53b0d -r 3904cfde1aa9 src/ZF/Constructible/DPow_absolute.thy --- a/src/ZF/Constructible/DPow_absolute.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/ZF/Constructible/DPow_absolute.thy Sun Mar 22 19:31:13 2020 +0000 @@ -581,7 +581,7 @@ ==> transrec_replacement(L, \x f u. \r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & big_union(L, r, u), j)" -apply (rule transrec_replacementI, assumption) +apply (rule L.transrec_replacementI, assumption) apply (unfold transrec_body_def) apply (rule strong_replacementI) apply (rule_tac u="{j,B,Memrel(eclose({j}))}" diff -r e30dbfa53b0d -r 3904cfde1aa9 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/ZF/Constructible/L_axioms.thy Sun Mar 22 19:31:13 2020 +0000 @@ -110,7 +110,7 @@ apply (rule Union_ax) done -interpretation L?: M_trivial L by (rule M_trivial_L) +interpretation L: M_trivial L by (rule M_trivial_L) (* Replaces the following declarations... lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L] diff -r e30dbfa53b0d -r 3904cfde1aa9 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/ZF/Constructible/Rec_Separation.thy Sun Mar 22 19:31:13 2020 +0000 @@ -184,7 +184,7 @@ theorem M_trancl_L: "M_trancl(L)" by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L]) -interpretation L?: M_trancl L by (rule M_trancl_L) +interpretation L: M_trancl L by (rule M_trancl_L) subsection\\<^term>\L\ is Closed Under the Operator \<^term>\list\\ @@ -371,7 +371,7 @@ apply (rule M_datatypes_axioms_L) done -interpretation L?: M_datatypes L by (rule M_datatypes_L) +interpretation L: M_datatypes L by (rule M_datatypes_L) subsection\\<^term>\L\ is Closed Under the Operator \<^term>\eclose\\ @@ -434,7 +434,7 @@ apply (rule M_eclose_axioms_L) done -interpretation L?: M_eclose L by (rule M_eclose_L) +interpretation L: M_eclose L by (rule M_eclose_L) end diff -r e30dbfa53b0d -r 3904cfde1aa9 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Sun Mar 22 19:31:13 2020 +0000 @@ -961,11 +961,11 @@ lemma formula_rec_replacement: \ \For the \<^term>\transrec\\ "[|n \ nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)" -apply (rule transrec_replacementI, simp add: nat_into_M) +apply (rule L.transrec_replacementI, simp add: L.nat_into_M) apply (rule strong_replacementI) apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}" in gen_separation_multi [OF formula_rec_replacement_Reflects], - auto simp add: nat_into_M) + auto simp add: L.nat_into_M) apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI) apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+ done diff -r e30dbfa53b0d -r 3904cfde1aa9 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Sun Mar 22 19:02:39 2020 +0000 +++ b/src/ZF/Constructible/Separation.thy Sun Mar 22 19:31:13 2020 +0000 @@ -304,7 +304,7 @@ theorem M_basic_L: " M_basic(L)" by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L]) -interpretation L?: M_basic L by (rule M_basic_L) +interpretation L: M_basic L by (rule M_basic_L) end