Commit Graph

351 Commits

Author SHA1 Message Date
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