172 Commits

Author	SHA1	Message	Date
Makarius Wenzel	afcd78610b	More concise export artifact	2022-12-04 18:03:53 +01:00
Makarius Wenzel	b8a9ef5118	Tuned comments	2022-12-04 16:38:56 +01:00
Makarius Wenzel	a4e75c8b12	Clarified export name for the sake of low-level errors	2022-12-04 16:35:55 +01:00
Makarius Wenzel	44cae2e631	More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports	2022-12-04 00:09:29 +01:00
Makarius Wenzel	e8c7fa6018	Clarified signature	2022-12-03 14:44:04 +01:00
Makarius Wenzel	912d4bb49e	Maintain document template in Isabelle/ML via Isar commands: ... result becomes export artifact, which is harvested by Isabelle/Scala build engine	2022-12-02 20:05:15 +01:00
Makarius Wenzel	a6c1a2baa4	Removed obsolete "extend" operation	2022-12-02 15:31:23 +01:00
Makarius Wenzel	cc3e2a51a4	More antiquotations	2022-12-02 13:50:16 +01:00
Makarius Wenzel	9e4e5b49eb	More antiquotations from Isabelle2021-1/2022	2022-12-02 11:41:31 +01:00
Makarius Wenzel	f44f0af01c	Use regular Toplevel.presentation from Isabelle2022, without alternative presentation hook	2022-12-01 22:48:45 +01:00
Makarius Wenzel	9a11baf840	Latex.output_name name is back in Isabelle2022	2022-12-01 22:04:56 +01:00
Nicolas Méric	06833aa190	Upddate single argument handling for compute_attr_access ... Trigger error when the attribute is not specified as an argument of the antiquatation and is not an attribujte of the instance. (In these case, the position of the attribute is NONE)	2022-11-28 10:05:47 +01:00
Nicolas Méric	4f0c7e1e95	Fix type unification clash for trace_attribute term antiquotation	2022-11-25 08:57:59 +01:00
Nicolas Méric	0040949cf8	Add trace-attribute term antiquotation ... - Make doc_class type and constant used by regular expression in monitors ground - Make class tag attribute ground (with serial()) - The previous items make possible the evaluation of the trace attribute and the definition of the trace-attribute term annotation	2022-11-24 16:47:21 +01:00
Nicolas Méric	e68c332912	Fix markup for some antiquotations ... Fix markup for docitem_attribute and trace_attribute ML and text antiquotations	2022-11-24 11:22:02 +01:00
Burkhart Wolff	b2c4f40161	Some LaTeX experiments with Achim	2022-11-18 10:30:33 +01:00
Burkhart Wolff	309952e0ce	syntactic rearrangements	2022-11-09 11:19:00 +01:00
Burkhart Wolff	830e1b440a	ported another Figure* in OutOfOrderPresntn to Isabelle2022	2022-11-09 06:06:30 +01:00
Burkhart Wolff	2149db9efc	semantics of fig_content (untested)	2022-11-08 20:52:58 +01:00
Burkhart Wolff	1547ace64b	added some semantics to fig_content	2022-11-08 19:27:07 +01:00
Burkhart Wolff	29770b17ee	added syntax for fig_content	2022-11-08 10:03:15 +01: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	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	9f2e2b53a4	Merge branch 'main' into Isabelle_dev	2022-08-01 22:58:21 +01: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
Achim D. Brucker	205aa5a6b1	Moved core ACM styles into DOF-core.sty.	2022-06-29 21:45:09 +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	a54373ad2f	Merge branch 'config_as_options'	2022-06-25 16:36:46 +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
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
Nicolas Méric	83c790d66a	Handle normalization of trace attribute	2022-05-26 12:56:21 +02:00
Nicolas Méric	9981c31966	Normalize docobj table value ... Normalize the record registered as value in the docobj table, i.e., the logical value of a docitem (a class instance)	2022-05-25 17:10:57 +02:00
Nicolas Méric	d8fde4b4f4	Cleanup and add test for meta-args for assert*	2022-04-19 14:05:52 +02:00
Achim D. Brucker	0f3f5d4b56	Fixed file attributes.	2022-04-17 16:32:12 +01:00
Nicolas Méric	74420a932f	Clean up check_invariants	2022-04-07 15:36:01 +02:00
Nicolas Méric	8e1702d2da	Add IDE reporting for attributes in meta-argument list	2022-04-07 15:33:24 +02:00
Nicolas Méric	b1f73e9235	Delete Isabelle marks file	2022-04-01 11:54:49 +02:00