718 Commits

All Branches

Search

Author	SHA1	Message	Date
Burkhart Wolff	3b4e82b27c	New autoref - format, ...	2019-05-28 10:43:40 +02:00
Burkhart Wolff	dce560b05a	Again Unsyncref; changes in thy_output in order to tackle duplicate meta_args_problem	2019-05-28 10:18:40 +02:00
Burkhart Wolff	c4a4ca3ffc	small im[provements of comments	2019-05-27 11:58:22 +02:00
Burkhart Wolff	88773050d3	eliminated bullocks	2019-05-27 11:44:30 +02:00
Burkhart Wolff	3919696521	eliminated bullocks.	2019-05-27 11:34:47 +02:00
Burkhart Wolff	d4bb579e09	added meta_args transmission	2019-05-27 11:18:21 +02:00
Burkhart Wolff	4e4d1a1aad	merge	2019-05-27 11:15:01 +02:00
Burkhart Wolff	9e396b4778	LaTeX Generator Crash resolved, many little changes...	2019-05-27 11:03:32 +02:00
Frédéric Tuong	d2e5bea25a	upgrade to Isabelle2018	2019-05-24 20:17:15 +02:00
Frédéric Tuong	447942ff6f	clean	2019-05-24 20:16:37 +02:00
Burkhart Wolff	ed1bef5cbf	some better trace infos over the LaTeX generator Bug	2019-05-23 15:17:24 +02:00
Burkhart Wolff	6b62e260cd	Diverse patches um den Crash des LaTeX generators zu verstehen.	2019-05-17 12:05:04 +02:00
Burkhart Wolff	cb72f2f16e	Diverse patches um den Crash des LaTeX generators zu verstehen.	2019-05-17 12:02:45 +02:00
Burkhart Wolff	803e97ce16	Experiments with the LaTeX generator	2019-05-14 09:13:42 +02:00
Burkhart Wolff	40537d4009	First Version with patched LaTeX Generator thy_output.ML	2019-04-29 22:24:32 +02:00
Burkhart Wolff	4a9e765cd3	second pass. Small errors here and there. Version in interactive mode for testing - no session Isa_DOF yet.	2019-04-29 17:32:45 +02:00
Burkhart Wolff	f89471d422	First Port of Isa_DOF to Isabelle2018 (without LaTeX Generation; Front-End Unit-Tested)	2019-04-29 17:06:03 +02:00
Burkhart Wolff	b035996d36	petitesse	2019-04-19 16:16:54 +02:00
Burkhart Wolff	76f86c5c0e	Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF	2019-04-18 17:16:08 +02:00
Burkhart Wolff	c752a25dd6	no message	2019-04-18 17:13:32 +02:00
Frédéric Tuong	e1ad1c39c6	upgrade to Isabelle2018 , synchronize with citadelle-devel 5bfebab420098b1083bf5b34a11b01e2f51e3568	2019-04-16 16:30:43 +02:00
Burkhart Wolff	436d41d232	Small things at CENELEC arising from FM paper. ... text_elem according to common discussopn with Achim.	2019-04-16 11:06:21 +02:00
Burkhart Wolff	3e3fc502c3	Ideas with Achim on text_elements + new elements in CENELEC	2019-04-11 19:40:10 +02:00
Achim D. Brucker	0789a96677	Dangling references and undefined citations are now breaking the document build.	2019-04-07 18:07:29 +01:00
Achim D. Brucker	40f5fa17d3	Add label for default text elements.	2019-04-07 17:42:35 +01:00
Achim D. Brucker	b0fbc80495	Excluded example of dangling reference from LaTex generation.	2019-04-07 17:41:41 +01:00
Achim D. Brucker	23e3486f5b	Bug fix: labels were missing int generated LaTeX.	2019-04-07 17:16:05 +01:00
Achim D. Brucker	0b3a361b06	Improved spacing for type-setting keywords.:	2019-04-06 19:47:44 +01:00
Achim D. Brucker	9d74c29f1d	Refactoring: moved LaTeX generation code in own structure.	2019-04-06 18:58:13 +01:00
Achim D. Brucker	783f580752	Added NOPs for ghost commands in the author section.	2019-04-06 13:40:38 +01:00
Achim D. Brucker	811dc0ef22	Added basic support for http_site attribute.	2019-04-06 13:30:36 +01:00
Achim D. Brucker	a36c1566d4	Fixed printing of default template.	2019-04-06 13:19:27 +01:00
Achim D. Brucker	da3ffdc729	"Renamed lipics template (currently not supported). ... This renaming should clearly communicate that this setup is not a (well) supported configuration. Firstly, lipics requires a recent version of comment.sty that conflicts with the outdated version required by Isabelle and, moreover, the lipics classes are non-free and, hence, prevent us from distribution a patched version that works with Isabelle.	2019-04-06 13:16:04 +01:00
Achim D. Brucker	00cb307fc5	Changed user interface of the installation script: supports now long and short options and allows one to skipt the lengthy patch and afp installation check.	2019-04-06 12:49:24 +01:00
Achim D. Brucker	090b5f3e63	Remove outdated aux file prior to starting the LateX build.	2019-04-06 12:32:30 +01:00
Burkhart Wolff	4a61b55763	merge	2019-04-06 12:16:36 +02:00
Burkhart Wolff	e362286c32	xcgdfg	2019-04-06 12:10:19 +02:00
Burkhart Wolff	4f349de9b9	some patches in install to make it run on MacOS	2019-04-06 12:08:38 +02:00
Achim D. Brucker	e4c1356a79	Fixed spelling in info/warning/error messages.	2019-04-06 10:23:30 +01:00
Achim D. Brucker	d5e295c7f3	Use cmp instead of md5sum for checking if files are identical.	2019-04-06 10:22:40 +01:00
Achim D. Brucker	9f3b406750	Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF	2019-04-06 10:04:58 +01:00
Achim D. Brucker	6995461742	Improved error handling during patch installation.	2019-04-06 10:04:44 +01:00
Frédéric Tuong	9a1bec2d85	Merge branch 'master' of git.logicalhacking.com:HOL-OCL/Isabelle_DOF	2019-04-04 15:44:15 +02:00
Frédéric Tuong	0d96aeb494	support inner syntax cartouches to prevent an error for accent letters in attributes (see hol-testgen/add-ons/Featherweight-OCL/src/compiler_generic/Init.thy )	2019-04-04 15:43:48 +02:00
Burkhart Wolff	5a0caa4163	Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF	2019-04-02 14:28:05 +02:00
Burkhart Wolff	83151cf473	Something in Isabelle_DOF	2019-04-02 14:19:59 +02:00
Achim D. Brucker	9d7ebc4a4f	Enabled passing of default arguments to LaTeX backend.	2019-03-31 17:47:10 +01:00
Achim D. Brucker	c3409d1f10	Cleanup: moved outdated code for exporting LaTeX style files into a dedicated functions and disabled file output.	2019-03-31 15:13:27 +01:00
Achim D. Brucker	0daaf3d699	Bug fix: subsubsection was mapped to subsection.	2019-03-31 14:08:52 +01:00
Achim D. Brucker	9edb344218	Added generic type hook.	2019-03-31 13:34:52 +01:00