From 06dddeacf57eb9fa39eac4aac383f6ac81423d18 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Wed, 10 Mar 2021 22:04:09 +0000
Subject: [PATCH] Porting to Isabelle 2021.

---
 .config                                                |  6 +++---
 README.md                                              | 10 +++++-----
 .../TR_MyCommentedIsabelle.thy                         |  6 +++---
 src/DOF/Isa_DOF.thy                                    |  6 ++++--
 ...tput.Isabelle2020.ML => thy_output.Isabelle2021.ML} |  0
 5 files changed, 15 insertions(+), 13 deletions(-)
 rename src/patches/{thy_output.Isabelle2020.ML => thy_output.Isabelle2021.ML} (100%)
 mode change 100755 => 100644

diff --git a/.config b/.config
index 692faa9..494272c 100755
--- a/.config
+++ b/.config
@@ -6,9 +6,9 @@ DOF_LATEST_DOI="10.5281/zenodo.3370483"
 DOF_GENERIC_DOI="10.5281/zenodo.3370482"
 #
 # Isabelle and AFP Configuration
-ISABELLE_VERSION="Isabelle2020: April 2020"
-ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2020/"
-AFP_DATE="afp-2020-04-20"
+ISABELLE_VERSION="Isabelle2021: February 2021"
+ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021/"
+AFP_DATE="afp-2021-03-09"
 AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
 #
 # Isabelle/DOF Repository Configuration
diff --git a/README.md b/README.md
index ce7e26d..23db051 100755
--- a/README.md
+++ b/README.md
@@ -20,10 +20,10 @@ foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-u
 
 Isabelle/DOF has two major pre-requisites:
 
-* **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020/).
-  Please download the Isabelle 2020 distribution for your operating
-  system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020/).
-* **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This
+* **Isabelle:** Isabelle/DOF requires [Isabelle 2021](http://isabelle.in.tum.de/website-Isabelle2021/).
+  Please download the Isabelle 2021 distribution for your operating
+  system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021/).
+* **LaTeX:** Isabelle/DOF requires a modern TeX-engine supporting the \expanded{}-primitive. This
   is, for example, included in the [TeXLive 2020](https://www.tug.org/texlive/) (or later)
   distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html)
   for installing TeXLive.
@@ -41,7 +41,7 @@ one), the full path to the ``isabelle`` command needs to be passed as
 using the ``--isabelle`` command line argument of the ``install`` script:
 
 ```console
-foo@bar:~$ ./install --isabelle /usr/local/Isabelle2020/bin/isabelle
+foo@bar:~$ ./install --isabelle /usr/local/Isabelle2021/bin/isabelle
 ```
 
 For further command line options of the installer, please use the
diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
index 190f91e..4054bbd 100755
--- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
+++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
@@ -1,7 +1,7 @@
 (*************************************************************************
  * Copyright (C) 
- *               2019      The University of Exeter 
- *               2018-2019 The University of Paris-Saclay
+ *               2019-2021 The University of Exeter 
+ *               2018-2021 The University of Paris-Saclay
  *               2018      The University of Sheffield
  *
  * License:
@@ -1196,7 +1196,7 @@ text\<open>
   Registers  \<^ML_type>\<open>Toplevel.transition -> Toplevel.transition\<close> parsers to the 
   Isar interpreter.\<close>
 
-text\<open>The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command definitions, with the 
+text\<open>The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command definitions, with the 
      all-important theory header declarations for outer syntax keywords.\<close>
 
 subsubsection*[ex1137::example]\<open>Examples: \<^theory_text>\<open>text\<close>\<close>
diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index 48604d5..6188ba5 100755
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -854,11 +854,13 @@ fun err msg pos = error (msg ^ Position.here pos);
 
 fun check_path check_file ctxt dir (name, pos) =
   let
-    val _ = Context_Position.report ctxt pos Markup.language_path;
+    val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be 
+                                                                                   "lifted" to 
+                                                                                   type source *)
 
     val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
     val _ = Path.expand path handle ERROR msg => err msg pos;
-    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
+    val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
     val _ =
       (case check_file of
         NONE => path
diff --git a/src/patches/thy_output.Isabelle2020.ML b/src/patches/thy_output.Isabelle2021.ML
old mode 100755
new mode 100644
similarity index 100%
rename from src/patches/thy_output.Isabelle2020.ML
rename to src/patches/thy_output.Isabelle2021.ML