Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
340 Commits 15 Branches 10 Tags 76 MiB
Commit Graph

86 Commits

Author SHA1 Message Date
Burkhart Wolff 906131da83 Kleinigkeiten repariert. 2018-10-04 17:45:39 +02:00
Burkhart Wolff b17110db7c comment inside meta_args problem solved. 2018-10-04 17:25:45 +02:00
Burkhart Wolff eaca1959ce Intermediate status : some spacing works. 2018-10-04 16:58:09 +02:00
Burkhart Wolff ac835ea028 First experiments with a more liberal LaTeX parser for meta-args. 2018-10-04 15:58:20 +02:00
Burkhart Wolff c0b27698ae Implemented ontology sty template generator. 2018-10-02 18:29:18 +02:00
Achim D. Brucker 484637d83c Removed Text*. 2018-10-02 00:35:50 +01:00
Achim D. Brucker a0d68b8e07 Hack: removing control characters and string quotes. 2018-09-18 17:17:02 +01:00
Achim D. Brucker a3065ab6f9 Changed type of figure width to integer. 2018-09-18 15:34:18 +01:00
Achim D. Brucker 1382d7c600 Restructured arguments for LaTeX invironments. 2018-09-18 14:26:19 +01:00
Achim D. Brucker ce1a6febfa Converted all *-commands to document_body. 2018-09-17 20:32:11 +01:00
Burkhart Wolff 385af317f3 Added appropriate type-checking for ISA docitems as well as another syntax docitem text antiquotation. 2018-09-17 16:48:05 +02:00
Burkhart Wolff 2e097e6b3c rough, non-functional implementation of ISA docitem 2018-09-11 14:15:11 +02:00
Burkhart Wolff 3a44b83ab9 Added new ISA’s and tests. Slight cleanup. 2018-09-11 13:51:25 +02:00
Burkhart Wolff 5eebf2ef5b some more isa’s 2018-09-11 12:08:25 +02:00
Burkhart Wolff f5117da8cb Achim & bu session on LaTeX Gen. 2018-09-11 11:35:25 +02:00
Burkhart Wolff e07b57dd95 Achim/Bu Telco debug. 2018-09-11 09:33:17 +02:00
Burkhart Wolff 0331c5dcbd Cleanup for the ISA infrastructure. 
Checking some Examples.
 2018-09-11 08:50:51 +02:00
Burkhart Wolff 2abb74c743 Added transducer function. 2018-09-03 21:31:06 +02:00
Burkhart Wolff d7794e06ac Added ISA_tables (inner syntax antiquotations) 
- Kleinkram.
 2018-09-03 20:56:08 +02:00
Burkhart Wolff 745b335033 small steps here and there 2018-08-30 12:53:02 +02:00
Burkhart Wolff 177938de0b Support for two more links/hoverings: 
- update_instance*[>omega<::E, … ]
-  @{docitem_attr a2::>omega<}
 2018-08-28 18:21:37 +02:00
Burkhart Wolff 86e145f723 - restructuring in IsaDOF : 
factoring out create_and_check_docitem
- correction IsaDofApplication
  side_by_side figure commented in and works.
- reaactivated open_monitor.
- changing types of monitor traces : simpler calculation now,
  but more obscure type
- first simulation of monitor trace construction.
 2018-08-27 14:39:34 +02:00
Burkhart Wolff 0914a1fc5c A little cleanup. 2018-08-24 22:02:04 +02:00
Burkhart Wolff 466552a3d7 - debugging calculations for mutated text items 
- cleanup
- a wee bit serious testing in Attributes.thy
  of this feature.
 2018-08-24 21:57:16 +02:00
Burkhart Wolff 0f36e8b761 Milestone reached: 
- further debugging
- all tests checked
- all examples running (after updates to current attribute conventions)
 2018-08-24 17:14:39 +02:00
Burkhart Wolff cedac17646 First reasonably well-tested version with 
- access of attributes for objects created over multiple
  inheritance
- taking updates into account
 2018-08-24 16:58:06 +02:00
Burkhart Wolff 25bcc030b4 Integrated new attribute calculation machinery. 
Sort of works, but problems with inheritance.
Downward incompatibility:
only either long-names or short names allowed for attributes,
but nothing in between.
 2018-08-24 15:49:13 +02:00
Burkhart Wolff 8fcc67978c Resolved the type inference riddle and worked out 
a solution (type matching and instantiation.)
Documented the interface to the type interface
in MyCommentedIsabelle with an example.
 2018-08-22 22:06:15 +02:00
Burkhart Wolff 627122c3fa New generalised attribute term constructor (untested) 
Refactoring necessary.
 2018-08-20 20:29:04 +02:00
Burkhart Wolff 5d7c32479d corrected DOF_core.get_attribute_info. 
Restructuring with this respect.
 2018-08-20 13:54:53 +02:00
Burkhart Wolff 00a4fd1c6b First attribute eval bug: 
- default terms now start from an undefined with
  correct ground type.
 2018-08-20 12:00:59 +02:00
Burkhart Wolff 4ffcf185ff Starting systematic testing and debugging of 
- default attribute construction
- attribute evaluation
 2018-08-20 11:36:04 +02:00
Burkhart Wolff 0bc3120dca Added new printing commands for doc_class and doc_item table. 2018-08-19 10:17:17 +02:00
Burkhart Wolff 7f032c439e Cleanups. 
Test environment for attribute evaluations.
 2018-08-18 14:44:39 +02:00
Burkhart Wolff b56c02cd6a Repaired bug in the meta-args parser. 
LaTeX generation for Text* environments with
antiquotation expansion works for the first time.
 2018-08-17 13:19:12 +02:00
Burkhart Wolff 1358540a62 Simplified thy_output (cleanup) and set first LaTeX meta-args generator. 
Restructuring
 2018-08-16 16:52:08 +02:00
Burkhart Wolff 0f12eb2e21 New configuration with modified Isabelle-LaTeX generator. 
Possesses Hook in order to parse meta attributes (not set so far,
default no-parse to empty string).
Current config compiles IsaDofApplications except Text*.
 2018-08-12 08:58:21 +02:00
Burkhart Wolff a07900bfab Some intermediate Hack to find a solution of the text* problem. 
textbis does both interactive and basically correct LaTeX generation
with antiquotation expansion.

At least a thing to study.

bu
 2018-07-12 12:08:58 +01:00
Burkhart Wolff bbf2ecb536 Kleinigkeiten um MathExam. 2018-06-27 09:12:50 +02:00
Burkhart Wolff 6277f44e75 Working on 
- the Toplevel sync problem for LaTeX output
- attribute computation
- various syntax issues
- examples.
 2018-06-26 17:40:08 +02:00
Burkhart Wolff a0fac2d75b Configuration a la chasse du LaTeX generation bug (having its origine in the 
Isar transaction engine).
 2018-06-19 17:37:31 +02:00
Burkhart Wolff bafc2405e9 this and that. 2018-06-14 15:35:14 +02:00
Achim D. Brucker f4c66cd085 Renamed sideBySideFigure to side_by_side_figure. 2018-06-11 18:34:41 +01:00
Burkhart Wolff 774a5f20e8 sideBySide 2018-06-11 18:10:45 +02:00
Burkhart Wolff ab127abe9a Eingeführter title etc. … 2018-06-11 17:35:12 +02:00
Burkhart Wolff 68afffe674 Modifs on Math-Exam. and Article. 
Preparing code-infrastructure for Attribute Evaluations.

Improved “MyCommented Isabelle”.
 2018-06-07 13:56:15 +02:00
Burkhart Wolff acc76bdd01 Forgotten in previous commit 2018-05-28 16:11:28 +02:00
Burkhart Wolff 5fd6261351 Restoring git state - inconsistent for whatever reason. 2018-05-28 16:10:20 +02:00
Burkhart Wolff d2d7605a17 - tinkering ROOT 
- activation of RegExps.
 2018-05-24 11:13:23 +02:00
Burkhart Wolff 6aa563df17 Added syntactic constants for classes (for proper 
regexp parsing support).
 2018-05-15 09:11:17 +02:00