Fri, 30 Aug 2013 11:00:46 +0200 |
wenzelm |
private copy (!) of etc/symbols for WWW_Find, which has its own interpretation of the file format;
|
file |
diff |
annotate
|
Tue, 20 Nov 2012 22:52:04 +0100 |
wenzelm |
support for symbol groups, retaining original order of declarations;
|
file |
diff |
annotate
|
Tue, 20 Nov 2012 21:01:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
Thu, 30 Jun 2011 13:21:41 +0200 |
wenzelm |
standardized use of Path operations;
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 23:21:24 +0200 |
wenzelm |
more tolerant Symbol.decode;
|
file |
diff |
annotate
|
Sun, 19 Jun 2011 22:52:49 +0200 |
wenzelm |
accept control symbols;
|
file |
diff |
annotate
|
Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
Sat, 13 Nov 2010 20:06:52 +0100 |
wenzelm |
qualified Symbol_Pos.symbol;
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
Fri, 20 Nov 2009 16:08:14 +0100 |
wenzelm |
standardized headers;
|
file |
diff |
annotate
|
Fri, 20 Nov 2009 18:36:44 +1100 |
kleing |
WWW_Find component: find_theorems via web browser
|
file |
diff |
annotate
|