Achim D. Brucker
7d5d8590c2
Cleanup.
2018-09-18 14:34:14 +01:00
Achim D. Brucker
42b993c289
Basic convertion to a setup without the Scala converter.
2018-09-18 14:29:54 +01:00
Achim D. Brucker
85f332fe5e
Removed scala converter.
2018-09-18 14:28:06 +01:00
Achim D. Brucker
1382d7c600
Restructured arguments for LaTeX invironments.
2018-09-18 14:26:19 +01:00
Achim D. Brucker
da7f286dd5
Removed scala converter.
2018-09-18 14:24:25 +01:00
Burkhart Wolff
7d3ecbdefe
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
...
Added stronger example show-case : a “association class” -like Link involving sub-typing.
2018-09-18 08:57:53 +02:00
Achim D. Brucker
ce1a6febfa
Converted all *-commands to document_body.
2018-09-17 20:32:11 +01:00
Achim D. Brucker
9c042361dd
Removed white spaces in *-commands (workaround for bug in Isa_Dof.
2018-09-17 20:30:19 +01:00
Burkhart Wolff
9ef1185add
Commenting the InnerSyntaxAntiquotqtion sample.
...
This Feature is complete for the moment .
2018-09-17 17:16:11 +02:00
Burkhart Wolff
7847f1cf01
Cleanup of file “InnerSyntaxAntiquotations”.
2018-09-17 16:58:38 +02: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
bb9c5a4f24
First version with inner-syntax checking infrastructure with just
...
one inner syntax antiquotation: file.
Works on some examples.
2018-09-06 12:07:37 +02:00
Burkhart Wolff
718b6ae1f0
small follower bug.
2018-09-03 21:32:13 +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
5e9e05a24a
small stuff
2018-08-28 17:35:52 +02:00
Burkhart Wolff
b6b94da82f
slight cleanup.
2018-08-28 12:48:07 +02:00
Burkhart Wolff
08b8c27949
Simulation Monitor
2018-08-27 17:28:40 +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
4e601acd45
comments
2018-08-24 21:58:32 +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
d04e09e24e
Solved type instantiation problem of future common value computation alg.
...
Commented il slow-motion in MyCommentedIsabelle.
2018-08-23 11:46:20 +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
8e09644e5c
increasing robustness of generic attribute term constructor
...
(adding antiquotations)
2018-08-21 08:07:07 +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
Achim D. Brucker
5eb298b389
Added isamarkupText*-environment for development purposes.
2018-08-10 14:27:30 +02:00
Burkhart Wolff
e81427061b
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
2018-07-12 12:09:24 +01: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
Achim D. Brucker
a1a99c314a
Fixed typos.
2018-07-02 22:23:05 +01:00
Burkhart Wolff
21cd7bbcfd
Added some commands in preamble.
...
Does not work yet.
2018-07-02 13:06:18 +02:00