| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 16:56:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 20:51:11 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 11:39:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 13:55:10 +0100 |
wenzelm |
clarified Token.check_src: intern at most once;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2015 13:45:11 +0100 |
wenzelm |
cartouche_declaration for Eisbach;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 17:23:47 +0200 |
wenzelm |
support for declaration within token source;
|
file |
diff |
annotate
|
| Wed, 20 Aug 2014 11:05:41 +0200 |
wenzelm |
support for nested Token.src within Token.T;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2014 18:02:34 +0200 |
wenzelm |
more informative Token.Name with history of morphisms;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 20:58:32 +0200 |
wenzelm |
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 17:54:09 +0200 |
wenzelm |
allow text cartouches in regular outer syntax categories "text" and "altstring";
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 12:25:17 +0100 |
wenzelm |
more markup for improper elements;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:27:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:13:38 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 16:11:47 +0100 |
wenzelm |
more explicit markup for Token.Literal;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 22:14:53 +0100 |
wenzelm |
tuned messages -- in accordance to Isabelle/Scala;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 22:08:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 21:40:39 +0100 |
wenzelm |
proper Args.syntax for slightly odd bundle trickery;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 20:27:08 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 18:06:23 +0100 |
wenzelm |
clarified Args.check_src: retain name space information for error output;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 16:30:07 +0100 |
wenzelm |
clarified Args.src: more abstract type, position refers to name only;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:30:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:20:41 +0100 |
wenzelm |
prefer Name_Space.pretty with its builtin markup;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 16:37:56 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|