merged;
authorwenzelm
Sat, 21 Mar 2020 22:12:21 +0100
changeset 71582 f2c1154e9c8d
parent 71581 e9f53182c4aa (diff)
parent 71565 24b68a932f26 (current diff)
child 71583 200ec7c4c1a5
merged;
NEWS
--- a/NEWS	Thu Mar 19 11:57:43 2020 +0100
+++ b/NEWS	Sat Mar 21 22:12:21 2020 +0100
@@ -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
--- a/src/Doc/Isar_Ref/Generic.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -1301,8 +1301,8 @@
 
   The rule \<open>P \<Longrightarrow> P \<or> Q\<close> is unsafe because it reduces \<open>P
   \<or> Q\<close> to \<open>P\<close>, which might turn out as premature choice of an
-  unprovable subgoal.  Any rule is unsafe whose premises contain new
-  unknowns.  The elimination rule \<open>\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q\<close> is
+  unprovable subgoal.  Any rule whose premises contain new unknowns is
+  unsafe. The elimination rule \<open>\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q\<close> is
   unsafe, since it is applied via elim-resolution, which discards the
   assumption \<open>\<forall>x. P x\<close> and replaces it by the weaker
   assumption \<open>P t\<close>.  The rule \<open>P t \<Longrightarrow> \<exists>x. P x\<close> is
@@ -1316,8 +1316,8 @@
   that \<open>(\<or>E)\<close> 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.
 
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -2434,7 +2434,7 @@
   Variant \<open>code nbe\<close> accepts also non-left-linear equations for
   \<^emph>\<open>normalization by evaluation\<close> only.
 
-  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
+  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
   and drop all code equations declared for them. In the case of \<open>abort\<close>,
   these constants then do not require to a specification by means of
   code equations; if needed these are implemented by program abort (exception)
--- a/src/Doc/Isar_Ref/Proof.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -1190,10 +1190,10 @@
   declared using the @{attribute_def induct_simp} attribute.
 
   The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables
-  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can
-  separate variables by ``\<open>and\<close>'' 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
+  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. It is possible
+  to separate variables by ``\<open>and\<close>'' 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 ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -194,7 +194,7 @@
   arguments; a syntactic abbreviation links the long form with the abstract
   version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
   t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local
-  abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the fixed parameter
+  abbreviation \<open>a \<equiv> c.a x\<close> in the target context (for the fixed parameter
   \<open>x\<close>).
 
   Theorems are exported by discharging the assumptions and generalizing the
@@ -365,7 +365,7 @@
   \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> 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 \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}
+  The \<open>import\<close> consists of a locale expression; see \secref{sec:locale-expr}
   above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are
   parameters of the defined locale. Locale parameters whose instantiation is
   omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> 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"}.
 \<close>
 
--- a/src/Doc/JEdit/JEdit.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -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>Isabelle2019\<close>). Thus @{tool jedit_client} can connect to the
+  name (e.g.\ \<^verbatim>\<open>Isabelle2020\<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
@@ -2194,6 +2194,24 @@
   \<^bold>\<open>Workaround:\<close> Use action @{action isabelle.draft} and print via the Web
   browser.
 
+  \<^item> \<^bold>\<open>Problem:\<close> Antialiased text rendering may show bad performance or bad
+  visual quality, notably on Linux/X11.
+
+  \<^bold>\<open>Workaround:\<close> The property \<^verbatim>\<open>view.antiAlias\<close> (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>\<open>view.antiAlias=subpixel HRGB\<close>: it can be much
+  faster than \<^verbatim>\<open>standard\<close>, but occasionally causes problems with odd color
+  shades. An alternative is to have \<^verbatim>\<open>view.antiAlias=standard\<close> and set a Java
+  system property like this:\<^footnote>\<open>See also
+  \<^url>\<open>https://docs.oracle.com/javase/10/troubleshoot/java-2d-pipeline-rendering-and-properties.htm\<close>.\<close>
+  @{verbatim [display] \<open>isabelle jedit -Dsun.java2d.opengl=true\<close>}
+
+  If this works reliably, it can be made persistent via @{setting
+  JEDIT_JAVA_OPTIONS} within \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. 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>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
   event handling of Java/AWT/Swing.
 
--- a/src/Doc/System/Environment.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/System/Environment.thy	Sat Mar 21 22:12:21 2020 +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/Isabelle2018\<close>.
+    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2020\<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>Isabelle2018\<close>''.
+  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020\<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 Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/System/Misc.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -11,6 +11,113 @@
   alphabetical order.
 \<close>
 
+section \<open>Building Isabelle docker images\<close>
+
+text \<open>
+  Docker\<^footnote>\<open>\<^url>\<open>https://docs.docker.com\<close>\<close> provides a self-contained environment
+  for complex applications called \<^emph>\<open>container\<close>, 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>\<open>\<^url>\<open>https://docs.docker.com/docker-for-windows\<close>\<close> and
+  macOS\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-mac\<close>\<close>. 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]
+\<open>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).\<close>}
+
+  Option \<^verbatim>\<open>-E\<close> sets \<^verbatim>\<open>bin/isabelle\<close> of the contained Isabelle distribution as
+  the standard entry point of the Docker image. Thus \<^verbatim>\<open>docker run\<close> will
+  imitate the \<^verbatim>\<open>isabelle\<close> command-line tool (\secref{sec:isabelle-tool}) of a
+  regular local installation, but it lacks proper GUI support: \<^verbatim>\<open>isabelle jedit\<close>
+  will not work without further provisions. Note that the default entrypoint
+  may be changed later via \<^verbatim>\<open>docker run --entrypoint="..."\<close>.
+
+  Option \<^verbatim>\<open>-t\<close> specifies the Docker image tag: this a symbolic name within the
+  local Docker name space, but also relevant for Docker
+  Hub\<^footnote>\<open>\<^url>\<open>https://hub.docker.com\<close>\<close>.
+
+  Option \<^verbatim>\<open>-l\<close> specifies the default logic image of the Isabelle distribution
+  contained in the Docker environment: it will be produced by \<^verbatim>\<open>isabelle build -b\<close>
+  as usual (\secref{sec:tool-build}) and stored within the image.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-B\<close> 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>\<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.
+
+  Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
+  of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
+
+  Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as
+  provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 18.04 LTS). This
+  imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will
+  only provide remote X11 support according to the modest GUI quality
+  standards of the late 1990-ies.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close>
+  outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a
+  Dockerfile only, which might be useful for informative purposes or other
+  tools.
+
+  Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  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>}
+
+  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>}
+
+  Invoke the raw Isabelle/ML process within that image:
+  @{verbatim [display]
+\<open>  docker run test/isabelle:Isabelle2020 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>}
+  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>
 
@@ -267,7 +374,7 @@
 
   \<^medskip>
   The default is to output the full version string of the Isabelle
-  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>.
+  distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020: April 2020\<close>.
 
   The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
   id of the @{setting ISABELLE_HOME} directory.
--- a/src/Doc/manual.bib	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/manual.bib	Sat Mar 21 22:12:21 2020 +0100
@@ -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}}
 }
--- a/src/Pure/PIDE/rendering.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -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)
 
--- a/src/Pure/System/isabelle_system.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -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
--- a/src/Pure/Thy/sessions.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -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,
--- a/src/Pure/Tools/build.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -294,7 +294,6 @@
             }
 
           process.result(
-            progress_stderr = Output.writeln(_),
             progress_stdout = (line: String) =>
               Library.try_unprefix("\floading_theory = ", line) match {
                 case Some(theory) =>
--- a/src/Pure/Tools/build_docker.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/build_docker.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -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),
--- a/src/Pure/Tools/dump.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -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 =
--- a/src/Pure/Tools/update.scala	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/update.scala	Sat Mar 21 22:12:21 2020 +0100
@@ -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)
 
--- a/src/Pure/thm_deps.ML	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/thm_deps.ML	Sat Mar 21 22:12:21 2020 +0100
@@ -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) =>
--- a/src/Tools/jEdit/src/jEdit.props	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sat Mar 21 22:12:21 2020 +0100
@@ -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
--- a/src/ZF/Constructible/AC_in_L.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -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 "\<forall>x[L]. \<exists>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 "\<exists>r. wellordered(L,x,r)" 
-    by (blast intro: well_ord_imp_relativized)
+    by (blast intro: L.well_ord_imp_relativized)
 qed
 
 text\<open>In order to prove \<^term>\<open> \<exists>r[L]. wellordered(L,x,r)\<close>, it's necessary to know 
--- a/src/ZF/Constructible/DPow_absolute.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -581,7 +581,7 @@
     ==> transrec_replacement(L, \<lambda>x f u. 
               \<exists>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}))}" 
--- a/src/ZF/Constructible/L_axioms.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -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]
--- a/src/ZF/Constructible/Rec_Separation.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -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\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>list\<close>\<close>
@@ -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\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>eclose\<close>\<close>
@@ -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
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -961,11 +961,11 @@
 lemma formula_rec_replacement: 
       \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
    "[|n \<in> 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
--- a/src/ZF/Constructible/Separation.thy	Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/Separation.thy	Sat Mar 21 22:12:21 2020 +0100
@@ -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