| Sun, 28 Apr 2019 13:09:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 19:48:29 +0200 |
wenzelm |
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 17:09:21 +0200 |
wenzelm |
support "tag" marker with scope;
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 17:45:00 +0100 |
wenzelm |
more accurate markup;
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 13:48:46 +0100 |
wenzelm |
documentation of document markers and re-interpreted command tags;
|
file |
diff |
annotate
|
| Sun, 17 Mar 2019 20:03:55 +0100 |
wenzelm |
more meta data from "dcterms" (superset of "dc");
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:31:24 +0100 |
wenzelm |
PIDE markup for spell-checking;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 14:19:30 +0100 |
wenzelm |
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 00:21:34 +0100 |
wenzelm |
added semantic document markers;
|
file |
diff |
annotate
|