Commit Graph

761 Commits

Author SHA1 Message Date
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
Achim D. Brucker 57923ad393 Removed all definitions that are semantically equivalent to their default variant. 2019-03-31 00:14:47 +00:00
Achim D. Brucker e26306debd Refactored LaTeX-Setup and introduced failback to default implementations. 2019-03-30 23:40:01 +00:00
Achim D. Brucker b5d35dad22 Added definition for SRAC. 2019-03-30 19:03:38 +00:00
Achim D. Brucker 8935d8f4e9 Improved error handling. 2019-03-30 17:18:17 +00:00
Achim D. Brucker 060dcbbabc Introduced \isadof* command family. 2019-03-30 16:36:25 +00:00
Achim D. Brucker 13db9a9e77 Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2019-03-25 12:23:00 +00:00
Achim D. Brucker 13b06fdce7 Added isaDof.subsection.scholarly_paper.conclusion. 2019-03-25 12:22:46 +00:00