| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 20:05:41 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 19:38:13 +0100 |
wenzelm |
added numeral, which supercedes num, xnum, float;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2008 19:27:42 +0100 |
wenzelm |
renamed terminal category "float" to "float_token", to avoid name
|
file |
diff |
annotate
|
| Sat, 29 Nov 2008 13:37:13 +0100 |
nipkow |
New lexical item "float".
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 21:26:41 +0200 |
wenzelm |
report_token/parse_token: back to context-less version;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 14:41:25 +0200 |
wenzelm |
ContextPosition.report;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 15:51:00 +0200 |
wenzelm |
token_kind: add Space, Comment;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 12:28:11 +0200 |
wenzelm |
pos_of_token: Position.T;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 00:09:35 +0200 |
wenzelm |
datatype token: maintain range, tuned representation;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 13:45:13 +0200 |
wenzelm |
improved position handling due to SymbolPos.T;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 16:43:26 +0200 |
wenzelm |
removed obsolete read_idents;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2008 22:27:27 +0100 |
wenzelm |
basic scanners: produce symbol list instead of imploded string;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:26:28 +0200 |
wenzelm |
replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
|
file |
diff |
annotate
|
| Mon, 13 Aug 2007 18:10:22 +0200 |
wenzelm |
Lexicon.tokenize: do not appen EndToken yet;
|
file |
diff |
annotate
|
| Thu, 12 Jul 2007 00:15:41 +0200 |
wenzelm |
sys_error;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:45 +0200 |
wenzelm |
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:18 +0200 |
wenzelm |
removed redundant string_of_vname (see term.ML);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:21 +0200 |
wenzelm |
avoid overloaded integer constants (accomodate Alice);
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 00:25:09 +0100 |
wenzelm |
read_xnum: return leading_zeros, radix;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 21:41:03 +0100 |
wenzelm |
xstr: disallow backslashes;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:07 +0200 |
wenzelm |
renamed Syntax.indexname to Syntax.read_indexname;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 12:12:08 +0200 |
wenzelm |
export is_tid;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 14:21:08 +0200 |
wenzelm |
uniform treatment of num/xnum;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:22:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 00:43:54 +0200 |
kleing |
hex and binary numerals (contributed by Rafal Kolanski)
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:38:00 +0200 |
wenzelm |
moved internal/skolem to term.ML;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:15 +0100 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Fri, 10 Feb 2006 02:22:50 +0100 |
wenzelm |
added fixedN, constN;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:16:10 +0100 |
wenzelm |
removed Syntax.deskolem;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:35 +0100 |
wenzelm |
added deskolem;
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:41 +0200 |
wenzelm |
moved is_ident to General/symbol.ML;
|
file |
diff |
annotate
|
| Tue, 17 May 2005 18:10:44 +0200 |
wenzelm |
added read_variable: optional question mark on input;
|
file |
diff |
annotate
|
| Mon, 16 May 2005 10:29:15 +0200 |
paulson |
Use of IntInf.int instead of int in most numeric simprocs; avoids
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 18 Jan 2005 14:36:04 +0100 |
berghofe |
indexname function now parses type variables as well; changed input
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:06:42 +0200 |
wenzelm |
Library.read_int; Output.output;
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:22:10 +0200 |
wenzelm |
string_of_vname moved to term.ML;
|
file |
diff |
annotate
|
| Tue, 11 May 2004 14:00:02 +0200 |
berghofe |
Eta-expanded function scan_comment to make SmlNJ happy.
|
file |
diff |
annotate
|
| Mon, 10 May 2004 19:26:58 +0200 |
wenzelm |
support nested comments;
|
file |
diff |
annotate
|
| Mon, 26 Apr 2004 15:00:20 +0200 |
wenzelm |
added is_ascii_identifier;
|
file |
diff |
annotate
|
| Fri, 07 Feb 2003 15:36:12 +0100 |
nipkow |
Added (* ... *) comments in formulae.
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 23:19:34 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:48:04 +0200 |
wenzelm |
added "num" token;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:19:40 +0200 |
wenzelm |
added read_xnum;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 11:36:29 +0200 |
wenzelm |
added internal, dest_internal;
|
file |
diff |
annotate
|
| Thu, 07 Oct 1999 14:32:32 +0200 |
wenzelm |
read_idents;
|
file |
diff |
annotate
|
| Sat, 04 Sep 1999 21:04:07 +0200 |
wenzelm |
removed binding;
|
file |
diff |
annotate
|
| Sat, 10 Jul 1999 21:40:14 +0200 |
wenzelm |
more specific exn;
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 10:40:23 +0100 |
wenzelm |
tuned usage of read;
|
file |
diff |
annotate
|
| Sat, 14 Nov 1998 13:23:49 +0100 |
wenzelm |
added read_nat;
|
file |
diff |
annotate
|
| Mon, 21 Sep 1998 10:43:54 +0200 |
paulson |
Unary minus is now #- and not #~
|
file |
diff |
annotate
|
| Mon, 10 Aug 1998 17:01:02 +0200 |
wenzelm |
dest_binding, dest_skolem;
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 10:28:44 +0200 |
wenzelm |
binding / skolem vars;
|
file |
diff |
annotate
|