Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
2,074 Commits 14 Branches 9 Tags 76 MiB
Commit Graph

709 Commits

Author SHA1 Message Date
Achim D. Brucker 5f5e8694d1 Updated root.tex files. 2019-01-06 14:38:05 +00:00
Achim D. Brucker 75ff2fad2d Revert "Removed obsolete build scripts." 
This reverts commit 30a17db2bf.
 2019-01-06 13:34:58 +00:00
Achim D. Brucker 30a17db2bf Removed obsolete build scripts. 2019-01-05 23:38:56 +00:00
Achim D. Brucker e0c5c81e1d Made upqoute and beramono optional. 2018-12-19 16:05:27 +00:00
Achim D. Brucker 87ee897983 Disabled upqoute - not part of texlive 2017. 2018-12-19 15:55:29 +00:00
Burkhart Wolff a1d6431df9 Added discussed ontology "math_paper" and an example reffering to (some elements) of it. 2018-12-19 12:05:57 +01:00
Achim D. Brucker 33bbd77f7a Disable math_exam examples - they are currently not supported. 2018-12-18 22:06:47 +00:00
Achim D. Brucker 860dab90f3 Removed generated output. 2018-12-18 22:05:07 +00:00
Burkhart Wolff eae495ac90 - Added monitor class-invariant for level consistency. 
- debugging here and there
- integration test
- remark : MathExam is in a pretty inconsistent state (requires discussion)
- integration test
 2018-12-18 14:29:08 +01:00
Burkhart Wolff 98565b837c Worked on assert*. 
Still needs debugging.
Regression tests of some examples;
necessary revisions due to stronger
checks at close_monitor.
 2018-12-11 16:03:01 +01:00
Burkhart Wolff 40c12801c6 Added finality check on monitor closes and check for open monitors in the global check. 2018-12-10 14:15:39 +01:00
Burkhart Wolff 25d79c1ba9 Added text antoquotations for attribute values and trace. 2018-12-07 13:17:39 +01:00
Burkhart Wolff 6f7e0a379d Better error messages of attribute accesses, 
regression test.
 2018-12-07 12:09:12 +01:00
Burkhart Wolff ffd7040495 Code Restructuring, Regression test. 2018-12-07 11:08:13 +01:00
Burkhart Wolff eda8535b1c - changed back ROOTS 
- IsaDof_Manual Monitor should be report.
 2018-12-06 12:31:12 +01:00
Achim D. Brucker 781c1ed0dc Manual merge. 2018-12-04 18:15:52 +00:00
Burkhart Wolff a5f9442c6e Added global command: check_doc_global 
(* checking unresolved forward references for the moment *)
 2018-12-04 15:04:50 +01:00
Burkhart Wolff 9c8d57e573 Continuous checking of class invariants of enabled monitors. 
Regression test suite revised.
 2018-12-04 14:28:59 +01:00
Burkhart Wolff 5e7ac1c02e - Fixed the FrontEnd - level problem according to what we discussed: 
-- there are classes that do not have a level
-- title, subtitle and abstract DO NOT HAVE a level
-- text* has a level, but the level "None"

- Tested whatever we have as examples
 2018-12-04 10:41:34 +01:00
Achim D. Brucker 459538a1b7 Figure group. 2018-12-04 06:05:49 +00:00
Achim D. Brucker 0f2dc58f5a Multi-file setup. 2018-12-04 05:31:45 +00:00
Burkhart Wolff 17c66f0fea Integrated is_monitor flag for monitor class invariants. 
Makes special treatment of monitor class invariants
possible, when changes of trace are indirect...
 2018-12-03 22:36:08 +01:00
Burkhart Wolff ac1180b529 - checking class invariants 
- checking monitor class invariants
 2018-12-03 22:18:47 +01:00
Burkhart Wolff 9c0bcd86c6 rearrangement 2018-12-03 16:48:15 +01:00
Burkhart Wolff dd942cfb99 rearrangement 2018-12-03 16:46:11 +01:00
Burkhart Wolff 04f5e99e41 First running example for class invariants. 2018-12-03 16:43:27 +01:00
Burkhart Wolff 184a17f977 Refinement: class invariants now gets also the oid from its context. 2018-12-03 14:25:04 +01:00
Burkhart Wolff 6b85bd74cd Very first example of class invariant checking ... 2018-12-03 14:14:53 +01:00
Burkhart Wolff 23bc75d08d Corrections in ontologies (revealed by examples) 
- identified problem: accept/reject conflicts were only detected at application
  time, not at declaration time :-( (leaved as "known problem" for the moment)
- new functionality for declaring doc class invariants
 2018-12-03 13:19:31 +01:00
Burkhart Wolff cf31ffd68b revisions of scholarly paper and report ontologies 2018-11-28 10:49:35 +01:00
Achim D. Brucker 25c295dd7f Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-11-27 14:22:19 +00:00
Achim D. Brucker 0b79c21d23 Upated title. 2018-11-27 14:18:54 +00:00
Achim D. Brucker d0d5567fc6 Restrucuring. 2018-11-27 13:51:12 +00:00
Achim D. Brucker 1f2551d683 Restrucuring. 2018-11-27 13:39:54 +00:00
Achim D. Brucker 21d51e7275 Restrucuring. 2018-11-27 13:22:31 +00:00
Achim D. Brucker 9d5bddea7c Restrucuring. 2018-11-27 13:11:54 +00:00
Achim D. Brucker b7e39f7d27 Initial commit. 2018-11-27 12:56:42 +00:00
Achim D. Brucker c32425a334 Added note about the state of the document. 2018-11-27 11:34:03 +00:00
Burkhart Wolff 8628ca81ab kleinkram 2018-11-27 11:13:49 +01:00
Achim D. Brucker bfdb5e5260 Restrucuring. 2018-11-27 09:41:04 +00:00
Achim D. Brucker eddc01e1c9 Cleanup. 2018-11-27 09:40:44 +00:00
Achim D. Brucker 0bc6f5521e Restrucuring. 2018-11-27 09:26:54 +00:00
Burkhart Wolff eea65018d1 Rearrangement of the group of TR examples. 
(following structure of math_exams)
 2018-11-21 11:15:21 +01:00
Burkhart Wolff 90f6c2d4ab - New checks for reject sets 
- basic infrastructure for class invariants
 2018-11-20 10:11:11 +01:00
Burkhart Wolff d406b3daeb implemented reject alphabets. (untested) 
slight corrections in MyCommentedIsabelle (MCI)
 2018-11-19 20:53:59 +01:00
Burkhart Wolff 0617315fb0 Small improvements on the term chapter of CommentedIsabelle 2018-11-19 11:32:22 +01:00
Burkhart Wolff f1eabf506c Changed the introduction of MyCommentedIsabelle 2018-11-15 15:20:22 +01:00
Burkhart Wolff 49d49cfcc4 New description of the goal package in the example (I had spare time in my FIIL exam). 2018-11-14 16:33:51 +01:00
Burkhart Wolff 256b2cac56 Exporting the .pdf version from the git-site: 2018-11-13 18:48:21 +01:00
Burkhart Wolff dcda1cc214 Introduced Syntax accept / reject. 
added some semantic for it (incomplete)
some elements on myCommentedIsabelle
 2018-11-13 15:19:02 +01:00
Burkhart Wolff 3a3e99ce98 Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-11-08 11:08:34 +01:00
Burkhart Wolff 027c501c0d Slight rearrangement in MyCommented. After some comments of readers. 2018-11-08 11:07:41 +01:00
Achim D. Brucker ea1480aecc Re-enabled use of side_by_side_figure. 2018-11-07 22:28:56 +00:00
Burkhart Wolff dd35fa356a Added new TR for MyCommentedIsabelle; many textual corrections. 2018-11-07 22:41:11 +01:00
Burkhart Wolff 18b8e35380 This and that. 2018-11-07 22:37:31 +01:00
Burkhart Wolff fe09c77b89 Moved MyCommentedIsabelle into the example/TR_my_commented isabelle 
- added build structure
- corrected LaTeX
- ... works as a first shot TR !!!
 2018-11-07 15:55:01 +01:00
Burkhart Wolff 3e6dc80445 - experiments with document ontologies 
- substantially more input on "MyCommentedIsabelle"
  (should be another TR example ? )
 2018-11-07 06:00:01 +01:00
Burkhart Wolff 8e216c02f2 wdfs 2018-11-06 11:05:11 +01:00
Achim D. Brucker 46c51235e3 Based all examples on session 'Functional-Automata'. 2018-11-06 09:31:01 +00:00
Achim D. Brucker ab3ba421c8 Fixed ROOT (removed dependency on non-existing ontology.tex. 2018-11-06 09:30:18 +00:00
Achim D. Brucker 4aa8730762 Updated ROOT(s) setup to include AFP entries ... 2018-11-06 09:10:11 +00:00
Burkhart Wolff 9494c05593 - Improved automata-management 
- automata transformation integrated
- control option strict_checking added
- rudimentary tests in IsaDofApplications and Monitor_Example
 2018-11-05 21:42:36 +01:00
Burkhart Wolff 8d9e6cdc48 Big Bang: Restructuring the RegExp Interface, pushing it underneath Isa_DOF, factoring out example into Monitor Example. 2018-11-04 19:15:22 +01:00
Burkhart Wolff 36fac27d0c New Config for 2017 including AFP contributions for Regular-Sets and Regular Automata. 
Added a thin layer interfacing these two.
Slight textual improvements of examples (updates to more recent notations).
 2018-10-30 15:50:01 +01:00
Achim D. Brucker c7665d4dd0 Promoted sections to chapters ... 2018-10-30 01:29:53 +00:00
Achim D. Brucker 55e8f84c77 Switched to technical report. 2018-10-30 00:59:47 +00:00
Achim D. Brucker c05bedf098 Initial setup. 2018-10-30 00:58:45 +00:00
Achim D. Brucker f69d388c49 Updated template. 2018-10-30 00:52:40 +00:00
Achim D. Brucker 862d487b90 Cleanup. 2018-10-30 00:27:07 +00:00
Achim D. Brucker 2923e996f8 Minor layout fixes. 2018-10-29 23:33:21 +00:00
Burkhart Wolff 58f2bff319 no message 2018-10-17 12:31:17 +02:00
Burkhart Wolff df4cf56958 Polish 2018-10-17 12:30:11 +02:00
Burkhart Wolff f1783538bd Cleanup with examples. More commendation. 
Another monitor example added (Concept_Example).
 2018-10-17 12:22:25 +02:00
Burkhart Wolff 0de079cfbb Special ML antiquotation for the trace attribute (a cleaned up version). 2018-10-16 12:23:36 +02:00
Burkhart Wolff 93074bf24d Trace-Calculation refined. One gets the additional information WHICH oid of which class 
is added to the trace.
 2018-10-16 10:44:59 +02:00
Burkhart Wolff 50ff554d53 Typo - correction 2018-10-11 14:55:57 +02:00
Burkhart Wolff 71a889ee58 Automatic trace attribute calculation works on both Attribute and IsaDofApplications. 2018-10-11 13:38:32 +02:00
Burkhart Wolff b220233373 doc_item creation detects enabled monitors … 2018-10-09 15:56:17 +02:00
Burkhart Wolff 8b6a1af99d Kleine Reparaturen hier und da, 
IsaDofApplications Paper weiter “Markupified”.
 2018-10-09 11:59:21 +02:00
Burkhart Wolff 2c80ff8d0a Substantial progress with monitors. 
- infra-structure open_monitor_tab
- computing of enabled ness
- semantics behind open and close monitor.
 2018-10-08 15:13:47 +02:00
Burkhart Wolff 04a354f10a Diverse Code-Massagen/Restruktorationen um Monitore vorzubereiten. 2018-10-08 10:30:53 +02:00
Burkhart Wolff b1e4e64e19 Global revision of the Isa_DOF state - representation as record. 
(Since more components are to come …)
Global revision of the entire example suite.
 2018-10-05 09:45:24 +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 e4bb874d86 More markdown in the IsaDofApplications example. 
The new setup is now checked on a Mac for the first time.
 2018-10-02 10:28:24 +02:00
Achim D. Brucker 61d69394c3 Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-10-02 08:14:23 +01:00
Achim D. Brucker 30e067ec0e Added types. 2018-10-02 08:08:47 +01:00
Achim D. Brucker 484637d83c Removed Text*. 2018-10-02 00:35:50 +01:00
Achim D. Brucker 910f81768f Build script that only copies style files into generation directory. 2018-09-18 17:18:15 +01:00
Achim D. Brucker 4c9c0a2bd1 Changed type of figure width to integer. 2018-09-18 15:34:33 +01:00
Achim D. Brucker 7d5d8590c2 Cleanup. 2018-09-18 14:34:14 +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 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 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 b6b94da82f slight cleanup. 2018-08-28 12:48:07 +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 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 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 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 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
Achim D. Brucker 86653eff41 Updated root.tex to latest version. 2018-06-29 10:21:00 +02:00
Burkhart Wolff 35a0a27c1d Kleinigkeiten. 2018-06-29 09:03:44 +02:00
Burkhart Wolff c0c92ac50c Vague pragmatics correction of the BAC example 2018-06-27 09:32:05 +02:00
Achim D. Brucker 02a697e6bb Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-06-27 09:18:44 +02:00
Achim D. Brucker c857160f04 Added figure. 2018-06-27 09:13:41 +02:00
Burkhart Wolff bbf2ecb536 Kleinigkeiten um MathExam. 2018-06-27 09:12:50 +02:00
Burkhart Wolff 2ff81dbb1c Repaired MathExam 
(well, commented out offending figure* declaration leading
to bugs in Backend.)
 2018-06-26 18:50:56 +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 aeb235447c Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-06-19 17:37:53 +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
Achim D. Brucker b7f2125202 Consistent use of Cartouch-delimiters. 2018-06-18 05:29:00 +01:00
Achim D. Brucker 038cd50045 Converted compactitem to itemize. 2018-06-18 05:24:01 +01:00
Achim D. Brucker f39cde669f Initial commit: CICM 2018 paper as example for the scholarly paper ontology. 2018-06-14 22:41:13 +01:00
Achim D. Brucker c78b8ba676 Removed outdated article example. 2018-06-14 22:27:21 +01:00
Idir AIT SADOUNE 9e6090c6a2 no message 2018-06-13 10:35:40 +02:00
Burkhart Wolff 862bb782ac Reworked MathExam. 2018-06-12 20:20:44 +02:00
Burkhart Wolff e804cff226 Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-06-12 10:10:04 +02:00
Burkhart Wolff e7a53276c5 Kleinkram 2018-06-12 10:09:36 +02:00
Achim D. Brucker bab84243d2 LaTeX support for monitors. 2018-06-12 08:45:37 +01:00
Achim D. Brucker f4c66cd085 Renamed sideBySideFigure to side_by_side_figure. 2018-06-11 18:34:41 +01:00
Achim D. Brucker b0d40de9a1 Updated LaTeX setup. 2018-06-09 15:24:17 +01:00
Burkhart Wolff 5d4ec26b5a Diskkussion with Achim 2018-06-08 17:42:58 +02:00
Burkhart Wolff 243545be5d Passt doch. 
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
 2018-06-08 17:12:45 +02:00
Achim D. Brucker d9228420e1 Port to Isabelle/DOF 0.0.3. 2018-06-08 14:41:16 +01:00
Burkhart Wolff 87fa4a975f iUpdated nach diskussion mit Achim 2018-06-08 12:13:45 +02:00
Burkhart Wolff ea4246a7a0 ncomplete checkin. Modifs on ROOT. 2018-06-08 11:46:44 +02:00
Burkhart Wolff cab810a8a6 Restructuring, and basic infrastructure for buildsRestructuring, and basic infrastructure for builds.. 2018-06-08 09:29:57 +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
Chantal Keller 7eb9082628 Merge branch 'master' of git.logicalhacking.com:HOL-OCL/Isabelle_DOF 2018-06-06 19:27:16 +02:00
Chantal Keller 30b3526fb2 BAC2017: more structure 2018-06-06 19:24:17 +02:00
Idir AIT SADOUNE 23db0e7568 no message 2018-06-06 12:00:22 +02:00
Chantal Keller 80f92c168c BAC2017: tried proofs 2018-06-06 08:37:06 +02:00
Chantal Keller 3b7a029d35 BAC2017: first two questions 2018-06-05 20:56:02 +02:00
Chantal Keller 49f1ed5200 BAC2017: removed errors 2018-06-05 19:20:00 +02:00
Burkhart Wolff d52c5090bd First correct attribute calculation. 2018-06-05 09:39:38 +02:00
Idir AIT SADOUNE b030859ddf no message 2018-06-04 14:46:11 +02:00
Idir AIT SADOUNE 7de68e7564 no message 2018-06-04 13:44:08 +02:00
Burkhart Wolff 37123100df Massage 2018-05-29 14:13:49 +02:00
Burkhart Wolff 1fd4f76fb3 Corrected sheet, added proof. 2018-05-29 14:03:07 +02:00
Burkhart Wolff ce17b1cf58 Repaired MathExam wrt. Ontology. 2018-05-29 12:02:13 +02:00
Burkhart Wolff 5fd6261351 Restoring git state - inconsistent for whatever reason. 2018-05-28 16:10:20 +02:00
Burkhart Wolff 0f32ddb71a Restructuring the example directory. Fixing math exa stuff. 2018-05-24 11:35:35 +02:00
Burkhart Wolff 93bad550ef Some library code for attribute accesses (not yet working) 
RegExp Expression Inner Syntax defined

RexExp Parsing activated.
 2018-05-11 15:51:26 +02:00
Burkhart Wolff 83222961a2 Weiss nicht was commit 2018-05-02 09:40:47 +02:00
Idir AIT SADOUNE 86cce02f7a no message 2018-04-30 13:13:53 +02:00
Burkhart Wolff 49e3ec81f7 Kleine Korrekturen an scholerly … 2018-04-30 10:48:14 +02:00
Burkhart Wolff 4d3371705c Typechecked , corrected and pimped up the MathExam scenario 
with solution sections and an adapted role model.
Added explanations
 2018-04-29 12:42:00 +02:00
Burkhart Wolff d9dd46f1ac Syntax for += works finally. 
Examples here and there…
 2018-04-29 11:35:24 +02:00
Burkhart Wolff 5ca263711c Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-04-29 09:55:21 +02:00
Burkhart Wolff 5ff40948af merge commit 2018-04-29 09:53:51 +02:00
Achim D. Brucker f5ef91fb72 Changed type of ORCID (non-option type, just string). 2018-04-28 21:45:02 +01:00
Achim D. Brucker b90df780fe Resolved merge conflict. 2018-04-28 17:44:06 +01:00
Achim D. Brucker 3587183a3f Renaming: keyword_list => keywordlist (to avoid LaTex special characters). 2018-04-28 17:42:16 +01:00
Burkhart Wolff be3c0fa315 worked on onto and instance of Conceptual example. 
For framework paper
 2018-04-28 15:15:25 +02:00
Burkhart Wolff 3e746a4d9d Typing works (more or less) for the value. 
Sometimes schematic variables were left-overs;
was able to suppress this type of fault by additional
annotations.
Sometimes confusion o heavily overloaded field names.
Also workaround by stronger annotations.
 2018-04-27 17:12:42 +02:00
Burkhart Wolff fb9da6784e Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-04-27 12:06:06 +02:00
Burkhart Wolff f01b36997e Version without type check and updated Article.thy 2018-04-27 12:05:22 +02:00
Idir AIT SADOUNE afc1518dde no message 2018-04-27 11:33:47 +02:00
Idir AIT SADOUNE 7a47c5702f Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 
# Conflicts:
#	examples/simple/Article.thy
 2018-04-27 11:16:41 +02:00
Idir AIT SADOUNE 01dac36275 no message 2018-04-27 11:15:27 +02:00
Burkhart Wolff 5bcd4c19b1 Intermediate Version 
- attribute value generation
- update interpreted
- type-checking integrated but crashes
- news on scholarly_paper …
 2018-04-27 10:34:24 +02:00
Burkhart Wolff 0474c47957 Thanks to a decisive Hint by Frederic Tuong: 
Managed to solve the Top-level-transaction problem
in “enriched_document_command”. Yay !!!
 2018-04-24 21:44:28 +02:00
Burkhart Wolff b54ed35466 Polishing in 3 and 4, micro-shortening, and new stuff in 4. 2018-04-22 13:47:29 +02:00
Burkhart Wolff 8ea00650a5 Minor corrections, refactoring, steps towards attribute calculation. 2018-04-19 11:04:11 +02:00
Burkhart Wolff 066396cfae Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF 2018-04-18 14:47:12 +02:00
Burkhart Wolff 99bdf17712 parsing and internal type-checking works. 
No integral type checking yet, and no execution.
 2018-04-18 14:46:28 +02:00
Idir AIT SADOUNE 2e185d9c25 no message 2018-04-18 09:36:21 +02:00
Idir AIT SADOUNE baa3ee9b45 no message 2018-04-17 16:43:08 +02:00
Burkhart Wolff 4c7a8ed91a kleinkram 2018-04-09 11:54:54 +02:00
Burkhart Wolff 64a1c82242 Diverses 2018-04-08 11:29:59 +02:00
Idir AIT SADOUNE c3a4111833 no message 2018-04-06 14:25:21 +02:00
Idir AIT SADOUNE 376c3fdd3b no message 2018-04-06 14:13:17 +02:00
Burkhart Wolff 46e1be6411 Added syntax for update_instance*… 
+= variant does not yet work.
 2018-04-05 12:44:52 +02:00
Burkhart Wolff 5e48dcffdf Ontology checking bug for unrelated direct sub_classes fixed. 
Enfin !
 2018-04-04 18:08:18 +02:00
Burkhart Wolff 027361fb03 unified syntax: 
renamed declare_reference open_monitor close_monitor
into declare_reference* open_monitor* close_monitor*
in order to simplify the task for Achim.
 2018-04-04 17:04:19 +02:00
Burkhart Wolff 229997d60a Added open/close monitor syntax. 2018-04-04 16:25:33 +02:00
Burkhart Wolff 4d09fc5e34 slight re-arrangement of the examples: 
the simple example becomes a cenelec example,
and simple got an example called Article based on
to the LNCS_onto.
 2018-04-04 16:14:37 +02:00
Burkhart Wolff 5bc9ddfd52 Running Version for Antiquotqtion Generation - 
with a Big - direct sons lead to false errors
 2018-04-04 14:44:21 +02:00
Burkhart Wolff 3338fffe19 General SML code cleanup. 
Further approximation to DocRef Generation.
 2018-04-04 10:45:56 +02:00
Burkhart Wolff f3f95fe112 added syntax for modes of doc_class_references. 
For forward-references, defining references, …

Global semantics untested and undocumented -> impl paper.

Preparative step for doc_class_reference generation.
 2018-03-29 11:19:07 +02:00
Burkhart Wolff 9dfa14eaea retouches 2018-03-28 21:08:37 +02:00
Burkhart Wolff 497c79349b Slight restructuring. 
Ontology instances in one site,
separated from the Isa_DOF core.
 2018-03-21 11:59:27 +01:00
Burkhart Wolff 868e6537db Kleinkram 
- ein paar Elemente im Parser
- neue tests im Exampl
 2018-03-14 18:03:35 +01:00
Burkhart Wolff a30e2061cd A decisive intermediate step: got sub-classing running, 
and pervasive point-and-click on doc-class references.

The entire thing starts to get presentable.
 2018-02-28 14:06:52 +01:00
Burkhart Wolff 6c59d9ba15 Refined the management of document classes and doc item refs. 
Refs were internally stored as global names.
Cross-Referencing over file-boundaries seems to work.
 2018-02-27 12:02:19 +01:00
Burkhart Wolff a64ed349d9 Added more checks. 
doc_class references now consequently based on short_names (for now).
 2018-02-09 12:25:15 +01:00
Burkhart Wolff 1d8872272b Management of doc_classes added, 
elementary checking of  doc-class referencing.
 2018-02-08 16:25:15 +01:00
Burkhart Wolff e29ee3789d Kind of current status. 
Crudely carved out of an other repository - not sure that this works.
 2018-02-07 19:44:27 +01:00