forked from Isabelle_DOF/Isabelle_DOF
Porting to Isabelle 2021.
This commit is contained in:
parent
e495a7b2fe
commit
06dddeacf5
6
.config
6
.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
|
||||
|
|
10
README.md
10
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
|
||||
|
|
|
@ -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>
|
||||
|
|
|
@ -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
|
||||
|
|
0
src/patches/thy_output.Isabelle2020.ML → src/patches/thy_output.Isabelle2021.ML
Executable file → Normal file
0
src/patches/thy_output.Isabelle2020.ML → src/patches/thy_output.Isabelle2021.ML
Executable file → Normal file
Reference in New Issue