forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'Isabelle_dev'
This commit is contained in:
commit
eac94f2a01
|
|
@ -15,4 +15,4 @@ It may also contain additional tools and script that are useful for preparing a
|
|||
* pdflatex
|
||||
* [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/browser_info/Unsorted/)
|
||||
* [aux files](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/)
|
||||
* [Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz)
|
||||
* [Isabelle_DOF-Unreleased_Isabelle2022.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2022.tar.xz)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
pipeline:
|
||||
build:
|
||||
image: docker.io/logicalhacking/isabelle2021-1
|
||||
image: docker.io/logicalhacking/isabelle2022
|
||||
commands:
|
||||
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
|
||||
- mkdir -p $ARTIFACT_DIR
|
||||
|
|
@ -16,7 +16,7 @@ pipeline:
|
|||
- cd ../..
|
||||
- ln -s * latest
|
||||
archive:
|
||||
image: docker.io/logicalhacking/isabelle2021-1
|
||||
image: docker.io/logicalhacking/isabelle2022
|
||||
commands:
|
||||
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
|
||||
- mkdir -p $ARTIFACT_DIR
|
||||
|
|
|
|||
|
|
@ -11,6 +11,8 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
|
|||
|
||||
### Changed
|
||||
|
||||
- Updated Isabelle version to Isabelle 2022
|
||||
|
||||
## [1.3.0] - 2022-07-08
|
||||
|
||||
### Changed
|
||||
|
|
|
|||
108
README.md
108
README.md
|
|
@ -1,46 +1,32 @@
|
|||
# [Isabelle/DOF](https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF): Document Preparation Setup
|
||||
|
||||
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
|
||||
Isabelle/DOF allows for both conventional typesetting as well as formal
|
||||
development. The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available
|
||||
Isabelle/DOF allows for both conventional typesetting and formal development.
|
||||
The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available
|
||||
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf)
|
||||
|
||||
## Pre-requisites
|
||||
|
||||
Isabelle/DOF has three major prerequisites:
|
||||
|
||||
* **Isabelle:** Isabelle/DOF requires [Isabelle 2021-1](http://isabelle.in.tum.de/website-Isabelle2021-1/).
|
||||
Please download the Isabelle 2021-1 distribution for your operating
|
||||
system from the [Isabelle
|
||||
website](http://isabelle.in.tum.de/website-Isabelle2021-1/).
|
||||
* **AFP:** Isabelle/DOF requires two entries from the [Archive of
|
||||
Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the
|
||||
AFP following the instructions given at
|
||||
<https://www.isa-afp.org/using.html>. For your convenience, we also
|
||||
provide a script that only installs the two entries required by
|
||||
Isabelle/DOF into the local Isabelle/DOF directory. First, Isabelle/DOF
|
||||
needs to be registered as an Isabelle component:
|
||||
|
||||
```console
|
||||
foo@bar:~$ isabelle components -u `pwd`
|
||||
```
|
||||
|
||||
Thereafter, the AFP entries can be installed as follows:
|
||||
|
||||
```console
|
||||
foo@bar:~$ isabelle env ./install-afp
|
||||
```
|
||||
|
||||
* **Isabelle:** Isabelle/DOF requires [Isabelle
|
||||
2022](http://isabelle.in.tum.de/website-Isabelle2022/). Please download the
|
||||
Isabelle 2022 distribution for your operating system from the [Isabelle
|
||||
website](http://isabelle.in.tum.de/website-Isabelle2022/).
|
||||
* **AFP:** Isabelle/DOF requires two entries from the [Archive of Formal Proofs
|
||||
(AFP)](https://www.isa-afp.org/). Please install the AFP following the
|
||||
instructions given at <https://www.isa-afp.org/using.html>.
|
||||
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
|
||||
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied.
|
||||
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates
|
||||
applied.
|
||||
|
||||
## Installation
|
||||
|
||||
Isabelle/DOF is provided as an Isabelle component. After installing the
|
||||
prerequisites, change into the directory containing Isabelle/DOF (this should be
|
||||
the directory containing this `README.md` file) and execute (if you executed
|
||||
this command already during the installation of the pre-requisites, you
|
||||
can skip it now):
|
||||
this command already during the installation of the prerequisites, you can skip
|
||||
it now):
|
||||
|
||||
```console
|
||||
foo@bar:~$ isabelle components -u `pwd`
|
||||
|
|
@ -58,25 +44,24 @@ This will compile Isabelle/DOF and run the example suite.
|
|||
|
||||
### Opening an Example
|
||||
|
||||
If you want to work with or extend one of the examples, e.g., you can
|
||||
open it similar to any standard Isabelle theory:
|
||||
If you want to work with or extend one of the examples, e.g., you can open it
|
||||
similar to any standard Isabelle theory:
|
||||
|
||||
```console
|
||||
isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
|
||||
```
|
||||
|
||||
This will open an example of a scientific paper using the pre-compiled
|
||||
session ``Isabelle_DOF``, i.e., you will not be able to edit the
|
||||
ontology definitions. If you want to edit the ontology definition,
|
||||
just open the theory file with the default HOL session:
|
||||
This will open an example of a scientific paper using the pre-compiled session
|
||||
``Isabelle_DOF``, i.e., you will not be able to edit the ontology definitions.
|
||||
If you want to edit the ontology definition, just open the theory file with the
|
||||
default HOL session:
|
||||
|
||||
```console
|
||||
isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
|
||||
```
|
||||
|
||||
While this gives you more flexibility, it might "clutter" your editing
|
||||
experience, as a lot of internal theories are loaded into Isabelle's
|
||||
editor.
|
||||
experience, as a lot of internal theories are loaded into Isabelle's editor.
|
||||
|
||||
### Creating a New Project
|
||||
|
||||
|
|
@ -87,23 +72,22 @@ Isabelle projects that use DOF need to be created using
|
|||
foo@bar:~$ isabelle dof_mkroot
|
||||
```
|
||||
|
||||
The ``dof_mkroot`` command takes the same parameter as the standard
|
||||
``mkroot`` command of Isabelle. Thereafter, the normal Isabelle
|
||||
command for building documents can be used.
|
||||
The ``dof_mkroot`` command takes the same parameter as the standard ``mkroot``
|
||||
command of Isabelle. Thereafter, the normal Isabelle command for building
|
||||
documents can be used.
|
||||
|
||||
Using the ``-o`` option, different ontology setups can be
|
||||
selected and using the ``-t`` option, different LaTeX setups
|
||||
can be selected. For example,
|
||||
Using the ``-o`` option, different ontology setups can be selected and using the
|
||||
``-t`` option, different LaTeX setups can be selected. For example,
|
||||
|
||||
```console
|
||||
foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl
|
||||
```
|
||||
|
||||
creates a setup using the scholarly_paper ontology and the article
|
||||
class from the KOMA-Script bundle.
|
||||
creates a setup using the scholarly_paper ontology and the article class from
|
||||
the KOMA-Script bundle.
|
||||
|
||||
The help (option ``-h``) show a list of all supported ontologies and
|
||||
document templates:
|
||||
The help (option ``-h``) show a list of all supported ontologies and document
|
||||
templates:
|
||||
|
||||
```console
|
||||
foo@bar:~$ isabelle dof_mkroot -h
|
||||
|
|
@ -128,7 +112,7 @@ are available:
|
|||
* [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz)
|
||||
* [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc)
|
||||
|
||||
### Older Releases
|
||||
### Older Releases
|
||||
|
||||
* Isabelle/DOF 1.2.0/Isabelle2021
|
||||
* [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
|
||||
|
|
@ -169,28 +153,32 @@ SPDX-License-Identifier: BSD-2-Clause
|
|||
|
||||
## Publications
|
||||
|
||||
* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
|
||||
Wolff. [Using The Isabelle Ontology Framework: Linking the Formal
|
||||
with the Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf).
|
||||
In Conference on Intelligent Computer Mathematics (CICM). Lecture
|
||||
Notes in Computer Science (11006), Springer-Verlag, 2018.
|
||||
* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff.
|
||||
[Using The Isabelle Ontology Framework: Linking the Formal with the
|
||||
Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf).
|
||||
In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in
|
||||
Computer Science (11006), Springer-Verlag, 2018.
|
||||
[doi:10.1007/978-3-319-96812-4_3](https://doi.org/10.1007/978-3-319-96812-4_3).
|
||||
|
||||
* Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and
|
||||
Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf).
|
||||
In Software Engineering and Formal Methods (SEFM). Lecture Notes in
|
||||
Computer Science (11724), Springer-Verlag, 2019.
|
||||
In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer
|
||||
Science (11724), Springer-Verlag, 2019.
|
||||
[doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
|
||||
|
||||
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In
|
||||
Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019.
|
||||
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments
|
||||
Targeting
|
||||
Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf).
|
||||
In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918).
|
||||
Springer-Verlag 2019.
|
||||
[doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)
|
||||
|
||||
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development
|
||||
Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document)
|
||||
In ERTS 2018. <https://hal.archives-ouvertes.fr/hal-01702815>
|
||||
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff.
|
||||
[Making Agile Development Processes fit for V-style Certification
|
||||
Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document). In ERTS
|
||||
2018. <https://hal.archives-ouvertes.fr/hal-01702815>
|
||||
|
||||
## Upstream Repository
|
||||
|
||||
The upstream git repository, i.e., the single source of truth, for this project is hosted
|
||||
at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.
|
||||
The upstream git repository, i.e., the single source of truth, for this project
|
||||
is hosted at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.
|
||||
|
|
|
|||
|
|
@ -8,5 +8,5 @@ sources = \
|
|||
src/scala/dof_mkroot.scala \
|
||||
src/scala/dof_tools.scala
|
||||
services = \
|
||||
isabelle_dof.DOF_Tools \
|
||||
isabelle_dof.DOF_Document_Build$Engine
|
||||
isabelle.dof.DOF_Tools \
|
||||
isabelle.dof.DOF_Document_Build$Engine
|
||||
|
|
|
|||
|
|
@ -12,8 +12,8 @@ option dof_version : string = "Unreleased"
|
|||
-- "Isabelle/DOF version"
|
||||
(* "Unreleased" for development, semantic version for releases *)
|
||||
|
||||
option dof_isabelle : string = "2021-1"
|
||||
option dof_afp : string = "afp-2021-12-28"
|
||||
option dof_isabelle : string = "2022"
|
||||
option dof_afp : string = "afp-2022-10-27"
|
||||
|
||||
option dof_latest_version : string = "1.3.0"
|
||||
option dof_latest_isabelle : string = "Isabelle2021-1"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -23,7 +23,7 @@ open_monitor*[this::report]
|
|||
(*>*)
|
||||
|
||||
title*[tit::title]\<open>My Personal, Eclectic Isabelle Programming Manual\<close>
|
||||
subtitle*[stit::subtitle]\<open>Version : Isabelle 2020\<close>
|
||||
subtitle*[stit::subtitle]\<open>Version : Isabelle 2022\<close>
|
||||
text*[bu::author,
|
||||
email = "''wolff@lri.fr''",
|
||||
affiliation = "\<open>Université Paris-Saclay, LRI, France\<close>"]\<open>Burkhart Wolff\<close>
|
||||
|
|
@ -1183,7 +1183,7 @@ text\<open> The extensibility of Isabelle as a system framework depends on a num
|
|||
\<^item> \<^ML>\<open>Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||||
adjoins a theory transformer.
|
||||
\<^item> \<^ML>\<open>Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||||
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||||
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\<close>
|
||||
\<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
|
||||
\<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
|
||||
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
|
||||
|
|
@ -1845,6 +1845,7 @@ text\<open>The second part is much more high-level, and can be found under \<^ML
|
|||
This is perhaps meant with the fairly cryptic comment:
|
||||
"Quasi-inner syntax based on outer tokens: concrete argument syntax of
|
||||
attributes, methods etc." at the beginning of this structure.\<close>
|
||||
ML\<open>open Args\<close>
|
||||
|
||||
text\<open> Some more combinators
|
||||
\<^item>\<^ML>\<open>Args.symbolic : Token.T parser\<close>
|
||||
|
|
@ -1865,12 +1866,11 @@ Common Isar Syntax
|
|||
\<^item>\<^ML>\<open>Args.name_position: (string * Position.T) parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.cartouche_inner_syntax: string parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.cartouche_input: Input.source parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.text_token: Token.T parser \<close>
|
||||
|
||||
|
||||
Common Isar Syntax
|
||||
\<^item>\<^ML>\<open>Args.text_input: Input.source parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.text : string parser\<close>
|
||||
\<^item>\<^ML>\<open>Parse.embedded_input: Input.source parser\<close>
|
||||
\<^item>\<^ML>\<open>Parse.embedded : string parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.binding : Binding.binding parser\<close>
|
||||
|
||||
Common Stuff related to Inner Syntax Parsing
|
||||
|
|
@ -1893,8 +1893,7 @@ Common Isar Syntax
|
|||
\<^item>\<^ML>\<open>Args.named_source: (Token.T -> Token.src) -> Token.src parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.named_typ : (string -> typ) -> typ parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.named_term : (string -> term) -> term parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.text_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.embedded_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.typ_abbrev : typ context_parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.typ: typ context_parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.term: term context_parser\<close>
|
||||
|
|
@ -1903,8 +1902,6 @@ Common Isar Syntax
|
|||
\<^item>\<^ML>\<open>Args.named_source: (Token.T -> Token.src) -> Token.src parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.named_typ : (string -> typ) -> typ parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.named_term: (string -> term) -> term parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.text_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||||
\<^item>\<^ML>\<open>Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\<close>
|
||||
|
||||
Syntax for some major Pure commands in Isar
|
||||
\<^item>\<^ML>\<open>Args.prop: term context_parser\<close>
|
||||
|
|
@ -2132,7 +2129,6 @@ Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to
|
|||
\<^item>\<^ML>\<open>Latex.string: string -> Latex.text\<close>
|
||||
\<^item>\<^ML>\<open>Latex.text: string * Position.T -> Latex.text\<close>
|
||||
|
||||
\<^item>\<^ML>\<open>Latex.output_name: string -> string\<close>
|
||||
\<^item>\<^ML>\<open>Latex.output_ascii: string -> string\<close>
|
||||
\<^item>\<^ML>\<open>Latex.output_symbols: Symbol.symbol list -> string\<close>
|
||||
|
||||
|
|
|
|||
23
install-afp
23
install-afp
|
|
@ -35,6 +35,8 @@ print_help()
|
|||
{
|
||||
echo "Usage: isabelle env ./install-afp [OPTION] "
|
||||
echo ""
|
||||
echo "Warning: This tools is deprecated."
|
||||
echo ""
|
||||
echo "Run ..."
|
||||
echo ""
|
||||
echo " --help, -h display this help message"
|
||||
|
|
@ -44,11 +46,29 @@ print_help()
|
|||
|
||||
exit_error() {
|
||||
echo ""
|
||||
echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***"
|
||||
echo " *** Local AFP installation FAILED, please check the README.md for help ***"
|
||||
echo ""
|
||||
exit 1
|
||||
}
|
||||
|
||||
confirm_usage() {
|
||||
echo "* From Isabelle2021-1 on, the recommended method for making the whole AFP "
|
||||
echo " available to Isabelle is the isabelle components -u command."
|
||||
echo " For doing so, please follow the instructions at: "
|
||||
echo " https://www.isa-afp.org/help/"
|
||||
echo ""
|
||||
echo " Alternatively, you can continue, on your own risk, to install only"
|
||||
echo " the AFP entries required to run Isabelle/DOF."
|
||||
echo ""
|
||||
read -p " Still continue (y/N)? " -n 1 -r
|
||||
echo
|
||||
if [[ $REPLY =~ ^[Yy]$ ]];
|
||||
then
|
||||
echo " Continuing installation on your OWN risk."
|
||||
else
|
||||
exit_error
|
||||
fi
|
||||
}
|
||||
check_isabelle_version() {
|
||||
echo "* Checking Isabelle version:"
|
||||
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
|
||||
|
|
@ -149,6 +169,7 @@ AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
|
|||
echo ""
|
||||
echo "Isabelle/DOF AFP Installation Utility"
|
||||
echo "====================================="
|
||||
confirm_usage
|
||||
check_isabelle_version
|
||||
check_afp_entries
|
||||
echo "* AFP Installation successful."
|
||||
|
|
|
|||
|
|
@ -206,7 +206,7 @@ fun check_latex_measure _ src =
|
|||
handle Fail _ => error ("syntax error in LaTeX measure") )
|
||||
in () end
|
||||
|
||||
val parse_latex_measure = Args.text_input >> (fn src => (check_latex_measure () (* dummy arg *) src;
|
||||
val parse_latex_measure = Parse.embedded_input >> (fn src => (check_latex_measure () (* dummy arg *) src;
|
||||
(fst o Input.source_content) src ) )
|
||||
|
||||
end\<close>
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019 The University of Exeter
|
||||
* 2018-2019 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -1965,6 +1965,23 @@ fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args
|
|||
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
|
||||
in markup (output_meta @ output_text) end;
|
||||
|
||||
val output_name = (* was available as Latex.output_name in Isabelle 2021-1 and earlier *)
|
||||
translate_string
|
||||
(fn "_" => "UNDERSCORE"
|
||||
| "'" => "PRIME"
|
||||
| "0" => "ZERO"
|
||||
| "1" => "ONE"
|
||||
| "2" => "TWO"
|
||||
| "3" => "THREE"
|
||||
| "4" => "FOUR"
|
||||
| "5" => "FIVE"
|
||||
| "6" => "SIX"
|
||||
| "7" => "SEVEN"
|
||||
| "8" => "EIGHT"
|
||||
| "9" => "NINE"
|
||||
| s => s);
|
||||
|
||||
|
||||
fun document_output_reports name {markdown, body} meta_args text ctxt =
|
||||
let
|
||||
val pos = Input.pos_of text;
|
||||
|
|
@ -1974,7 +1991,7 @@ fun document_output_reports name {markdown, body} meta_args text ctxt =
|
|||
(pos, Markup.plain_text)];
|
||||
fun markup xml =
|
||||
let val m = if body then Markup.latex_body else Markup.latex_heading
|
||||
in [XML.Elem (m (Latex.output_name name), xml)] end;
|
||||
in [XML.Elem (m (output_name name), xml)] end;
|
||||
in document_output {markdown = markdown, markup = markup} meta_args text ctxt end;
|
||||
|
||||
|
||||
|
|
@ -2364,7 +2381,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
|
|||
{unchecked = false, define= false} (* default *);
|
||||
|
||||
|
||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input))
|
||||
val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Parse.embedded_input))
|
||||
: ({define:bool,unchecked:bool} * Input.source) context_parser;
|
||||
|
||||
|
||||
|
|
@ -2835,7 +2852,7 @@ fun string_2_theory_text_antiquotation ctxt text =
|
|||
end
|
||||
|
||||
fun gen_text_antiquotation name reportNcheck compile =
|
||||
Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
||||
Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||
(fn ctxt => fn text:Input.source =>
|
||||
let
|
||||
val _ = reportNcheck ctxt text;
|
||||
|
|
@ -2848,7 +2865,7 @@ fun std_text_antiquotation name (* redefined in these more abstract terms *) =
|
|||
|
||||
(* should be the same as (2020):
|
||||
fun text_antiquotation name =
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||
(fn ctxt => fn text =>
|
||||
let
|
||||
val _ = report_text ctxt text;
|
||||
|
|
@ -2864,7 +2881,7 @@ fun std_theory_text_antiquotation name (* redefined in these more abstract terms
|
|||
|
||||
(* should be the same as (2020):
|
||||
fun theory_text_antiquotation name =
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||
(fn ctxt => fn text =>
|
||||
let
|
||||
val keywords = Thy_Header.get_keywords' ctxt;
|
||||
|
|
@ -2886,12 +2903,11 @@ fun theory_text_antiquotation name =
|
|||
|
||||
|
||||
fun environment_delim name =
|
||||
("%\n\\begin{" ^ Latex.output_name name ^ "}\n",
|
||||
"\n\\end{" ^ Latex.output_name name ^ "}");
|
||||
("%\n\\begin{" ^ Monitor_Command_Parser.output_name name ^ "}\n",
|
||||
"\n\\end{" ^ Monitor_Command_Parser.output_name name ^ "}");
|
||||
|
||||
fun environment_block name = environment_delim name |-> XML.enclose;
|
||||
|
||||
|
||||
fun enclose_env verbatim ctxt block_env body =
|
||||
if Config.get ctxt Document_Antiquotation.thy_output_display
|
||||
then if verbatim
|
||||
|
|
@ -2902,6 +2918,7 @@ fun enclose_env verbatim ctxt block_env body =
|
|||
end
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
local
|
||||
val parse_literal = Parse.alt_string || Parse.cartouche
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@ ML\<open>
|
|||
fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f))
|
||||
val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args)
|
||||
val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files))
|
||||
val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files
|
||||
val ml_content = map (fn f => Syntax.read_input (Bytes.content (#content f))) ml_files
|
||||
fun eval ml_content = fold (fn sml => (ML_Context.exec
|
||||
(fn () => ML_Context.eval_source ML_Compiler.flags sml)))
|
||||
ml_content
|
||||
|
|
|
|||
|
|
@ -28,10 +28,9 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*/
|
||||
|
||||
package isabelle_dof
|
||||
package isabelle.dof
|
||||
|
||||
import isabelle._
|
||||
import java.io.{File => JFile}
|
||||
|
||||
|
||||
object DOF_Document_Build
|
||||
|
|
@ -50,31 +49,31 @@ object DOF_Document_Build
|
|||
val directory = context.prepare_directory(dir, doc, latex_output)
|
||||
|
||||
// produced by alternative presentation hook (workaround for missing Toplevel.present_theory)
|
||||
for (name <- context.document_theories) {
|
||||
for {
|
||||
name <- context.document_theories.iterator
|
||||
entry <- context.session_context.get(name.theory, Export.DOCUMENT_LATEX + "_dof")
|
||||
} {
|
||||
val path = Path.basic(Document_Build.tex_name(name))
|
||||
val xml =
|
||||
YXML.parse_body(context.get_export(name.theory, Export.DOCUMENT_LATEX + "_dof").text)
|
||||
if (xml.nonEmpty) {
|
||||
File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic))
|
||||
.write(directory.doc_dir)
|
||||
}
|
||||
val xml = YXML.parse_body(entry.text)
|
||||
File.content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic))
|
||||
.write(directory.doc_dir)
|
||||
}
|
||||
val dof_home= Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME"));
|
||||
val isabelle_dof_dir = context.session_context.sessions_structure("Isabelle_DOF").dir
|
||||
// print(context.options.string("dof_url"));
|
||||
|
||||
// copy Isabelle/DOF LaTeX templates
|
||||
val template_dir = dof_home + Path.explode("src/document-templates/")
|
||||
val template_dir = isabelle_dof_dir + Path.explode("document-templates")
|
||||
// TODO: error handling in case 1) template does not exist or 2) root.tex does already exist
|
||||
val template = regex.replaceAllIn(context.options.string("dof_template"),"")
|
||||
Isabelle_System.copy_file(template_dir + Path.explode("root-"+template+".tex"),
|
||||
directory.doc_dir+Path.explode("root.tex"))
|
||||
|
||||
// copy Isabelle/DOF LaTeX styles
|
||||
val doc_jdir = new JFile(directory.doc_dir.implode)
|
||||
val styles = File.find_files(new JFile(dof_home.implode),((f:JFile) => f.getName().endsWith(".sty")), true)
|
||||
for (sty <- styles) {
|
||||
Isabelle_System.copy_file(sty, doc_jdir)
|
||||
}
|
||||
// copy Isabelle/DOF LaTeX styles
|
||||
List(Path.explode("DOF/latex"), Path.explode("ontologies"))
|
||||
.flatMap(dir =>
|
||||
File.find_files((isabelle_dof_dir + dir).file,
|
||||
file => file.getName.endsWith(".sty"), include_dirs = true))
|
||||
.foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file))
|
||||
|
||||
// create ontology.sty
|
||||
val ltx_styles = context.options.string("dof_ontologies").split(" +").map(s => regex.replaceAllIn(s,""))
|
||||
|
|
@ -83,7 +82,7 @@ object DOF_Document_Build
|
|||
|
||||
// create dof-config.sty
|
||||
File.write(directory.doc_dir+Path.explode("dof-config.sty"), """
|
||||
\newcommand{\isabelleurl}{https://isabelle.in.tum.de/website-Isabelle2021-1/""" + context.options.string("dof_isabelle") + """}
|
||||
\newcommand{\isabelleurl}{https://isabelle.in.tum.de/website-Isabelle2022/""" + context.options.string("dof_isabelle") + """}
|
||||
\newcommand{\dofurl}{""" + context.options.string("dof_url") + """}
|
||||
\newcommand{\dof@isabelleversion}{""" + context.options.string("dof_isabelle") + """}
|
||||
\newcommand{\isabellefullversion}{""" + context.options.string("dof_isabelle") + """\xspace}
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@
|
|||
Prepare session root directory for Isabelle/DOF.
|
||||
*/
|
||||
|
||||
package isabelle_dof
|
||||
package isabelle.dof
|
||||
|
||||
import isabelle._
|
||||
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@
|
|||
*/
|
||||
|
||||
|
||||
package isabelle_dof
|
||||
package isabelle.dof
|
||||
|
||||
import isabelle._
|
||||
|
||||
|
|
|
|||
|
|
@ -244,7 +244,7 @@ fun string_2_theory_text_antiquotation ctxt text =
|
|||
end
|
||||
|
||||
fun gen_text_antiquotation name reportNcheck compile =
|
||||
Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
||||
Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||
(fn ctxt => fn text:Input.source =>
|
||||
let
|
||||
val _ = reportNcheck ctxt text;
|
||||
|
|
@ -257,7 +257,7 @@ fun std_text_antiquotation name (* redefined in these more abstract terms *) =
|
|||
|
||||
(* should be the same as (2020):
|
||||
fun text_antiquotation name =
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||
(fn ctxt => fn text =>
|
||||
let
|
||||
val _ = report_text ctxt text;
|
||||
|
|
@ -273,7 +273,7 @@ fun std_theory_text_antiquotation name (* redefined in these more abstract terms
|
|||
|
||||
(* should be the same as (2020):
|
||||
fun theory_text_antiquotation name =
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
|
||||
(fn ctxt => fn text =>
|
||||
let
|
||||
val keywords = Thy_Header.get_keywords' ctxt;
|
||||
|
|
|
|||
Loading…
Reference in New Issue