Achim D. Brucker
873151b4f3
Update to Isabelle 2022.
2022-10-30 17:56:15 +00:00
Achim D. Brucker
cfdbd18bfa
Resolved merge conflict.
2022-10-30 11:52:41 +00:00
Achim D. Brucker
0b807ea4bc
Merge branch 'main' into Isabelle_dev
2022-10-30 11:22:13 +00:00
Makarius Wenzel
516f5d2f79
Merely use session structure instead of component settings.
2022-10-24 22:11:30 +02:00
Makarius Wenzel
5ac41a72ac
More accurate treatment of sty files: do not just copy from all examples.
2022-10-24 21:58:10 +02:00
Makarius Wenzel
15feeb7d92
More standard package name: appears to work properly in Isabelle2022.
2022-10-24 21:38:01 +02:00
Makarius Wenzel
0c8a0e1d63
Adapted to Isabelle/1ac2416e8432 -- approx. Isabelle2022 release.
2022-10-24 21:30:49 +02:00
Burkhart Wolff
0aec98b95a
cell row column parser setup
2022-10-11 21:43:13 +02:00
Burkhart Wolff
43871ced48
text-term* and text-value* antiquotation syntax, and more on tables.
2022-10-11 21:00:33 +02:00
Burkhart Wolff
0fa1048d6d
description of the tab model.
2022-10-10 13:51:54 +02:00
Burkhart Wolff
33490f8f15
table cell syntax implemented; roughly tested.
2022-10-09 14:01:53 +02:00
Burkhart Wolff
01632b5251
hoisting cm pt syntax intp COL
2022-10-06 16:59:42 +02:00
Burkhart Wolff
8a54831295
more elements for table parser.
2022-10-03 08:23:05 +02:00
Burkhart Wolff
427226f593
some stuff with tables
2022-09-27 12:16:31 +02:00
Achim D. Brucker
7f500dc257
Migration to latest Isabelle development version.
2022-08-11 23:04:07 +01:00
Achim D. Brucker
9f2e2b53a4
Merge branch 'main' into Isabelle_dev
2022-08-01 22:58:21 +01:00
Burkhart Wolff
583636404f
renamed cenelec_document into cenelec_report.
2022-08-01 21:50:49 +02:00
Burkhart Wolff
8a9684590a
pass through miniôdo: deeper ontological reasoning, less LaTeX.
2022-08-01 21:42:32 +02:00
Burkhart Wolff
81c4ae2c13
first version of new commands onto_class // doc_class
2022-08-01 15:53:33 +02:00
Achim D. Brucker
f40d33b9ed
Ad-hoc port to development version of Isabelle.
2022-07-17 22:46:56 +01:00
Achim D. Brucker
6a94728747
Port to development version of Isabelle.
2022-07-17 20:47:17 +01:00
Burkhart Wolff
c8a3c58f7f
end of discussion with Achim
2022-06-30 12:58:49 +02:00
Achim D. Brucker
b24ede4400
LIPIcs needs to stay unsupported, right now.
2022-06-29 21:46:39 +01:00
Achim D. Brucker
205aa5a6b1
Moved core ACM styles into DOF-core.sty.
2022-06-29 21:45:09 +01:00
Achim D. Brucker
c8f3bfc65d
Removed unused imports.
2022-06-29 20:17:40 +01:00
Achim D. Brucker
44f9317b35
Integrated dof-common.tex into DOF-core.sty.
2022-06-29 20:12:32 +01:00
Achim D. Brucker
6c2a0d6876
Renaming to ensure compliance with naming restrictions.
2022-06-29 19:08:56 +01:00
Achim D. Brucker
6c0d325673
Use full qualified name for templates.
2022-06-26 19:06:49 +01:00
Achim D. Brucker
b40069bedd
Use full qualified name for templates.
2022-06-26 19:06:45 +01:00
Achim D. Brucker
9ded308371
Use full qualified name for scholarly_paper.
2022-06-26 17:12:09 +01:00
Achim D. Brucker
e6ca682114
Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
2022-06-26 16:01:57 +01:00
Burkhart Wolff
013296f25e
experiments on tables
2022-06-26 13:48:03 +02:00
Achim D. Brucker
7c50ffb3af
Refactoring.
2022-06-25 17:15:04 +01:00
Achim D. Brucker
3a9826901a
Cleanup.
2022-06-25 17:11:01 +01:00
Achim D. Brucker
a54373ad2f
Merge branch 'config_as_options'
2022-06-25 16:36:46 +01:00
Achim D. Brucker
a973707a73
Implemented -h.
2022-06-24 17:02:12 +01:00
Achim D. Brucker
e138855623
Use comment.sty in LaTeX mode by default.
2022-06-24 16:07:25 +01:00
Achim D. Brucker
5278608b89
Merging main into config_as_options.
2022-06-24 15:57:59 +01:00
Achim D. Brucker
59658cea6f
mkroot_DOF is not replaced by dof_mkroot, which is implemented in Scala.
2022-06-24 14:55:53 +01:00
Achim D. Brucker
ef674b5ae2
Migrated, tested, and debugged new configuration setup.
2022-06-24 14:48:49 +01:00
Achim D. Brucker
ac8c939179
Initial setup using configurations as options, retiring both the build script (LaTeX build) and the mkroo_DOF script (replaced by a Scala-based tooling).
2022-06-24 14:02:19 +01:00
Burkhart Wolff
c16ec333f1
experiments on multi-commands - multi-figures
2022-06-24 08:15:03 +02:00
Burkhart Wolff
d1e4fd173b
Experiments with multi-commands and -figures.
...
- added multi-arg syntax (only one arg evaluated so far)
- added figure_content built-in antiquotation
- added new Figure* - multi-arg command.
2022-06-22 16:32:31 +02:00
Burkhart Wolff
43c857af2c
roughly ported Latex testbench to 21-1
2022-06-17 20:35:32 +02:00
Burkhart Wolff
0cc010cecc
debugged merge
2022-06-17 09:37:43 +02:00
Burkhart Wolff
ba7bd6dc03
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
2022-06-17 09:31:29 +02:00
Burkhart Wolff
43b0a3049f
Modelling sample for tables
2022-06-17 09:31:17 +02:00
Nicolas Méric
03fd491d5d
Implement CENELEC Table A.1
...
- Add an eager and lazy invariants checking functions mechanism
for low level invariants to allow the checking of invariants
only when opening or closing a monitor instance.
The state of the monitor instances traces evolves when declaring
instances between open_monitor* and close_monitor* commands.
This mechanism can capture the changes be defining
invariants before or after traces are populated but not
before and after, with the current mechanism.
Two tables were added: docclass_eager_inv_tab
and docclass_lazy_inv_tab to store these invariants
- Implement CENELEC_50128 Table A.1 using this mechanism
2022-06-13 07:56:53 +02:00
Nicolas Méric
9673359688
Enable high level invariants checking for some commands
...
Enable high level invariants checking for the update_instance*
and close_monitor* commands
2022-05-27 17:14:17 +02:00
Nicolas Méric
5d1b271336
Allow access to the monitor table for low level invariants
...
When defining low level invariants checking functions,
access to the monitor table might be useful.
So the table should be populated before the checking takes place.
2022-05-27 14:46:04 +02:00