wenzelm [Tue, 12 Aug 2008 21:28:03 +0200] rev 27842
abstract type span, tuned interfaces;
added report_token, report_span;
markup ident tokens;
wenzelm [Tue, 12 Aug 2008 21:28:01 +0200] rev 27841
adapted ThyEdit operations;
wenzelm [Tue, 12 Aug 2008 21:27:59 +0200] rev 27840
added ignored, malformed transitions;
wenzelm [Tue, 12 Aug 2008 21:27:57 +0200] rev 27839
Symbol.source/OuterLex.source: more explicit do_recover argument;
scan: pass position;
removed obsolete prepare_command (now inlined in isar_syn.ML);
renamed prepare_command_failsafe to prepare_command, reports tokens;
load_thy: now based on ThyEdit operations, reports tokens and spans;
tuned;
wenzelm [Tue, 12 Aug 2008 21:27:55 +0200] rev 27838
Isabelle.command: inline former OuterSyntax.prepare_command;
Isar.command: based on fail-safe OuterSyntax.prepare_command;
wenzelm [Tue, 12 Aug 2008 21:27:53 +0200] rev 27837
load thy_edit.ML before outer_syntax.ML;
wenzelm [Tue, 12 Aug 2008 21:27:51 +0200] rev 27836
renamed unknown_span to malformed_span;
added ident;
tuned;
wenzelm [Tue, 12 Aug 2008 21:27:48 +0200] rev 27835
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm [Tue, 12 Aug 2008 21:27:46 +0200] rev 27834
updated generated file;
haftmann [Mon, 11 Aug 2008 22:25:45 +0200] rev 27833
rudimentary code setup for set operations
wenzelm [Mon, 11 Aug 2008 22:06:51 +0200] rev 27832
<applet>: more XHTML 1.0 Transitional conformance;
wenzelm [Mon, 11 Aug 2008 22:06:49 +0200] rev 27831
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
wenzelm [Mon, 11 Aug 2008 20:56:32 +0200] rev 27830
<pre>: removed xml:space, is already default;
result(s): avoid improper nesting of <pre> within <p>;
wenzelm [Mon, 11 Aug 2008 18:37:51 +0200] rev 27829
produce XHTML 1.0 Transitional;
tuned charset name;
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
wenzelm [Mon, 11 Aug 2008 18:37:49 +0200] rev 27828
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
wenzelm [Mon, 11 Aug 2008 17:37:48 +0200] rev 27827
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
haftmann [Mon, 11 Aug 2008 14:50:04 +0200] rev 27826
changed code setup
haftmann [Mon, 11 Aug 2008 14:50:02 +0200] rev 27825
re-arranged class dense_linear_order
haftmann [Mon, 11 Aug 2008 14:50:00 +0200] rev 27824
rudimentary code setup for set operations
haftmann [Mon, 11 Aug 2008 14:49:53 +0200] rev 27823
moved class wellorder to theory Orderings
wenzelm [Sun, 10 Aug 2008 12:38:26 +0200] rev 27822
added parse_token (from proof_context.ML);
wenzelm [Sun, 10 Aug 2008 12:38:25 +0200] rev 27821
read_tyname/const/const_proper: report position;
moved parse_token to syntax.ML;
tuned;
wenzelm [Sun, 10 Aug 2008 12:38:24 +0200] rev 27820
pass position to get_fact;
tuned;
wenzelm [Sun, 10 Aug 2008 12:38:23 +0200] rev 27819
pass token source to typ/term etc.;
wenzelm [Sun, 10 Aug 2008 12:38:22 +0200] rev 27818
added name property operation;
added local_fact;
renamed proposition to prop (again);
wenzelm [Sat, 09 Aug 2008 22:43:59 +0200] rev 27817
renamed ML_Lex.val_of to content_of;
wenzelm [Sat, 09 Aug 2008 22:43:58 +0200] rev 27816
unified Args.T with OuterLex.token, renamed some operations;
moved thm_sel to attrib.ML;
wenzelm [Sat, 09 Aug 2008 22:43:57 +0200] rev 27815
unified Args.T with OuterLex.token;
RESET_VALUE of primitive parsers;
export keyword_with;
renamed keyword_sid to keyword_ident_or_symbolic;
added int (from args.ML);
added enum(1)', and_list(1)' (formerly in args.ML);
removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);
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);