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

154 Commits

Author SHA1 Message Date
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
Burkhart Wolff 2acc4ea222 Neue commands, import RegExp, … 2018-05-14 15:47:16 +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 49e3ec81f7 Kleine Korrekturen an scholerly … 2018-04-30 10:48:14 +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 b90df780fe Resolved merge conflict. 2018-04-28 17:44:06 +01:00
Achim D. Brucker f437e1337c Disable markdown. 2018-04-28 17:41:34 +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 f01b36997e Version without type check and updated Article.thy 2018-04-27 12:05:22 +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 eae6eaf005 Added “hidden tag fields” in order to make doc-classes disjoint 
Added overriding semantics and
overloading checks.
 2018-04-20 13:19:50 +02:00
Burkhart Wolff 8ea00650a5 Minor corrections, refactoring, steps towards attribute calculation. 2018-04-19 11:04:11 +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
Burkhart Wolff 7aa52c3fa1 Finally solved the problem with the type conformance of default values to declared attribute types. 2018-04-17 17:39:16 +02:00
Burkhart Wolff 18c0f6f06d Commented out attribute conformance check since problems. 2018-04-17 15:08:01 +02:00
Burkhart Wolff 731fd9c775 Diverses 2018-04-16 17:00:31 +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 f8692dd801 Renamed LNCS_onto into “scholarly_paper”. 
Decided for the trace variant semantics of monitors.
(more power, easier to implement)
 2018-04-05 12:09:58 +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 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 7305efc159 Added slightly better popup explanation for document classes. 2018-03-28 17:05:01 +02:00
Burkhart Wolff df5bf507cf Some more elements for a *parser* of LaTeX. 
>>>>>>>>>>>>>>>>>

import scala.util.parsing.combinator.Parsers
import scala.util.parsing.input.{NoPosition, Position, Reader}

object LaTeXParser extends Parsers {
  override type Elem = LaTeXToken

class LaTeXTokenReader(tokens: Seq[LaTeXToken]) extends Reader[Seq[LaTeXToken]] {
  override def first: Seq[LaTeXToken] = tokens.head::Nil
  override def atEnd: Boolean = tokens.isEmpty
  override def pos:   Position = NoPosition
  override def rest:  Reader[Seq[LaTeXToken]] = new LaTeXTokenReader(tokens.tail)
}
}

compiles, but the rest does not work. Unknown parsers etc.
Pb apparently with importing.
 2018-03-28 13:08:55 +02:00
Burkhart Wolff 38f8772a6a derniers touches 2018-03-28 09:24:27 +02: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 9686a7597a Lots of debugging 
Sub-Classing Works
 2018-02-28 11:31:42 +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