Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds the ability to rename inference rules when Tex filtering. #106

Open
wants to merge 49 commits into
base: master
Choose a base branch
from
Open

Adds the ability to rename inference rules when Tex filtering. #106

Changes from all commits
Commits
Show all changes
49 commits
Select commit Hold shift + click to select a range
58f5248
Adds the ability to rename inference rules when Tex filtering.
heades Dec 14, 2019
9b43236
Merge remote-tracking branch 'upstream/master'
heades Nov 16, 2020
b1ad0eb
Trims whitespace from around custom homs that interfers with Pandoc.
heades Nov 16, 2020
db4f53e
Removed a change that is not needed.
heades Nov 24, 2020
c94aa62
Undid the wrong patch. This adds in the patch for fixing whitespace
heades Nov 24, 2020
84d2f78
Fixed a bug in the renaming. Thanks @dorchard.
heades Feb 23, 2021
fff9fc9
Identifiers can now contain greek characters
phanukaev Aug 5, 2022
42b6c99
Merge pull request #1 from phanukaev/master
heades Aug 15, 2022
bfd9e93
fix README broken link found by Shaked
PeterSewell Mar 16, 2021
7e27d38
Make JSON pp optional, add warnings/errors on missing pp homs
bacam Mar 17, 2021
c3edcbb
fix X documentation
PeterSewell Jul 21, 2021
215f7d2
Fix make clean
tperami Mar 3, 2022
60eeb79
Remove executability of tests/test-mjp.ott
tperami Mar 3, 2022
4738a9a
Refer to PPrint instead of PPrintEngine and PPrintCombinators.
fpottier Jan 3, 2022
a80f257
tests/menhir_tests: refer to PPrint instead of PPrintEngine.
fpottier Jan 3, 2022
fa772b3
Update the copies of PPrint bundled in tests/menhir_tests/.
fpottier Jan 3, 2022
2c13c51
Enable automated testing of the OCaml code generation
kit-ty-kate Jan 3, 2022
154140d
Add relative path to ott binary in 1Bsemantics example
k4rtik Aug 19, 2020
6e3ecec
Allow recent PPrint version in opam file
tperami Mar 3, 2022
6140722
Remove embedded PPrint and add corresponding opam tests
tperami Mar 3, 2022
b050336
make README slightly more informative
PeterSewell Mar 4, 2022
88e93b3
coq-ott compatible with Coq 8.14
pi8027 Oct 27, 2021
5b5f033
Fix regression machinery for Coq
tperami Mar 7, 2022
1b613be
Allow recent Coq version with coq-ott in opam
tperami Mar 7, 2022
9adb532
Require minimum version of menhir
tperami Mar 7, 2022
ffc4521
Add new regression baseline for March 2022
tperami Mar 7, 2022
77245fd
Fix tests/test1.ott for Isabelle
tperami Mar 7, 2022
839c641
Update baseline for test1 fix
tperami Mar 8, 2022
d6e329f
Fix addition of extra pipe characters with isasyn
jvanbruegge Jul 7, 2020
94cc0c6
Fix opam file
tperami Mar 9, 2022
8c333f1
Bump to version 0.32
tperami Mar 9, 2022
1b4f322
rebuild manual
PeterSewell Mar 9, 2022
cf58898
Bump version number in opam file to 0.32
tperami Mar 9, 2022
3ebf936
Fix typo in README.md
tperami Apr 25, 2022
848f8dd
Update maintainer
tperami Apr 25, 2022
addb3e2
Fit licence and deps in ott.opam
tperami Apr 25, 2022
ae6c828
Add lex-comment hom to specify the comment start
tperami Oct 4, 2022
cb60f1d
OCaml 5.0 compatibility
bacam Nov 24, 2022
c4872aa
Add missing dependency on ocamlgraph, update OCaml version
bacam Nov 24, 2022
4723365
minimal _CoqProject change to enable compatibility with Coq 8.17 and …
palmskog Dec 1, 2022
4ce0e70
Bump version to 0.33
bacam Jan 16, 2023
0eef860
Rebuild documentation
bacam Jan 16, 2023
5cd7470
Support bytecode targets in opam
bacam Jan 18, 2023
24d2ea5
Update release instructions a little
bacam Jan 19, 2023
d6f97e4
Fix dead links to papers in README
omasanori Feb 16, 2023
1c8d2aa
Fix opam build on Windows (MinGW cygwin cross)
MSoegtropIMC Dec 14, 2023
c213235
The commands for renaming rules are better named.
heades Mar 9, 2024
a55a5fa
Merge branch 'ott-lang:master' into master
heades Mar 9, 2024
1baa0de
Undoing some changes.
heades Mar 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 8 additions & 3 deletions src/defns.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,11 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
"\\text{"
^ String.concat "" (Grammar_pp.apply_hom_spec m xd hs [])
^ "}") in
Printf.fprintf fd "\\newcommand{\\%sRenameRule%s}[0]{%s{%s}}\n"
(Grammar_pp.pp_tex_NAME_PREFIX m)
(Grammar_pp.tex_command_escape dr.drule_name)
(Grammar_pp.pp_tex_DRULE_NAME_NAME m)
(Auxl.pp_tex_escape dr.drule_name);
Printf.fprintf fd "\\newcommand{%s}[1]{%s[#1]{%%\n"
(Grammar_pp.tex_drule_name m dr.drule_name)
(Grammar_pp.pp_tex_DRULE_NAME m);
Expand All @@ -241,9 +246,9 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
(snd ppd_premises);
output_string fd "}{\n";
output_string fd ppd_conclusion;
Printf.fprintf fd "}{%%\n{%s{%s}}{%s}%%\n}}\n"
(Grammar_pp.pp_tex_DRULE_NAME_NAME m)
(Auxl.pp_tex_escape dr.drule_name)
Printf.fprintf fd "}{%%\n{\\%sRenameRule%s}{%s}%%\n}}\n"
(Grammar_pp.pp_tex_NAME_PREFIX m)
(Grammar_pp.tex_command_escape dr.drule_name)
pp_com
| Isa _ | Hol _ | Lem _ | Coq _ | Twf _ ->
let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in
Expand Down