wenzelm [Sat, 09 Aug 2008 22:43:56 +0200] rev 27814
unified Args.T with OuterLex.token;
renamed val_of to content_of;
added InternalValue kind;
added datatype value/slot with static binding (from args.ML);
renamed is_sid to ident_or_symbolic;
wenzelm [Sat, 09 Aug 2008 22:43:55 +0200] rev 27813
unified Args.T with OuterLex.token, renamed some operations;
removed obsolete parse_args (cf. parse);
wenzelm [Sat, 09 Aug 2008 22:43:54 +0200] rev 27812
unified Args.T with OuterLex.token, renamed some operations;
unified version of thm_sel (formerly in args.ML and spec_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:53 +0200] rev 27811
unified Args.T with OuterLex.token;
moved datatype value/slot and basic operations to outer_lex.ML;
removed unused terminator;
removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML);
removed obsolete thm_sel (cf. attrib.ML);
one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:52 +0200] rev 27810
load args.ML later (after outer_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:46 +0200] rev 27809
unified Args.T with OuterLex.token, renamed some operations;
wenzelm [Sat, 09 Aug 2008 12:28:13 +0200] rev 27808
read_asts: report literal tokens;
wenzelm [Sat, 09 Aug 2008 12:28:12 +0200] rev 27807
tuned error message;
wenzelm [Sat, 09 Aug 2008 12:28:11 +0200] rev 27806
pos_of_token: Position.T;
removed unused display_token;
tuned;
wenzelm [Sat, 09 Aug 2008 12:28:10 +0200] rev 27805
dest: sort strings;
report: Output.status;
wenzelm [Sat, 09 Aug 2008 12:28:09 +0200] rev 27804
added literal;
wenzelm [Sat, 09 Aug 2008 00:09:39 +0200] rev 27803
read_token: more robust handling of empty text;
wenzelm [Sat, 09 Aug 2008 00:09:38 +0200] rev 27802
datatype token: maintain range, tuned representation;
moved eof, stopper to lexicon.ML;
wenzelm [Sat, 09 Aug 2008 00:09:36 +0200] rev 27801
datatype token: maintain range, tuned representation;
tuned messages;
wenzelm [Sat, 09 Aug 2008 00:09:35 +0200] rev 27800
datatype token: maintain range, tuned representation;
added eof, stopper (from simple_parse.ML);
str_of_token: no special case for EOF;
misc tuning;
wenzelm [Sat, 09 Aug 2008 00:09:34 +0200] rev 27799
tuned SymbolPos interface;
wenzelm [Sat, 09 Aug 2008 00:09:31 +0200] rev 27798
YXML.parse: allow text without markup, potentially empty;
wenzelm [Sat, 09 Aug 2008 00:09:29 +0200] rev 27797
added content;
simplified implode: interface and permissive padding via Position.distance_of;
added range;
renamed implode_delim to implode_range;
wenzelm [Sat, 09 Aug 2008 00:09:26 +0200] rev 27796
added distance_of (permissive version);
added no_range;
tuned;
wenzelm [Fri, 08 Aug 2008 19:29:01 +0200] rev 27795
count offset as well;
more uniform treatment of invalid fields;
tuned;
wenzelm [Fri, 08 Aug 2008 19:28:59 +0200] rev 27794
added offset/end_offset;
wenzelm [Fri, 08 Aug 2008 16:54:33 +0200] rev 27793
tuned formatting;
krauss [Fri, 08 Aug 2008 15:36:40 +0200] rev 27792
clean up dead code
wenzelm [Fri, 08 Aug 2008 13:36:44 +0200] rev 27791
made SML/NJ happy;
krauss [Fri, 08 Aug 2008 09:44:16 +0200] rev 27790
FundefLib.try_proof : attempt a proof and see if it works
nipkow [Fri, 08 Aug 2008 09:26:15 +0200] rev 27789
added lemmas
wenzelm [Thu, 07 Aug 2008 23:56:45 +0200] rev 27788
inner_syntax markup is back;
wenzelm [Thu, 07 Aug 2008 23:32:49 +0200] rev 27787
disabled inner_syntax markup for now;
wenzelm [Thu, 07 Aug 2008 22:32:03 +0200] rev 27786
added read_token -- with optional YXML encoding of position;
tuned parse operations: print position instead of echoing input (now encoded!);
do not export obsolete read operation;
wenzelm [Thu, 07 Aug 2008 22:32:01 +0200] rev 27785
parse_token: use Syntax.read_token, pass full position information;