Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
Sat, 10 Jan 2009 13:10:38 +0100 |
wenzelm |
load_thy: explicit after_load phase for presentation;
|
file |
diff |
annotate
|
Wed, 07 Jan 2009 12:08:22 +0100 |
wenzelm |
added local_theory';
|
file |
diff |
annotate
|
Fri, 02 Jan 2009 16:21:47 +0100 |
wenzelm |
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
|
file |
diff |
annotate
|
Fri, 02 Jan 2009 15:44:33 +0100 |
wenzelm |
added type 'a parser, simplified signature;
|
file |
diff |
annotate
|
Tue, 30 Sep 2008 23:31:36 +0200 |
wenzelm |
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
|
file |
diff |
annotate
|
Tue, 30 Sep 2008 22:02:50 +0200 |
wenzelm |
load_thy: Toplevel.excursion based on units of command/proof pairs;
|
file |
diff |
annotate
|
Tue, 30 Sep 2008 14:19:25 +0200 |
wenzelm |
simplified process_file, eliminated Toplevel.excursion;
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 19:52:37 +0200 |
wenzelm |
P.doc_source and P.ml_sorce for proper SymbolPos.text;
|
file |
diff |
annotate
|
Wed, 13 Aug 2008 20:57:30 +0200 |
wenzelm |
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
|
file |
diff |
annotate
|
Tue, 12 Aug 2008 21:27:57 +0200 |
wenzelm |
Symbol.source/OuterLex.source: more explicit do_recover argument;
|
file |
diff |
annotate
|
Mon, 11 Aug 2008 22:06:49 +0200 |
wenzelm |
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
|
file |
diff |
annotate
|
Thu, 07 Aug 2008 13:45:07 +0200 |
wenzelm |
updated type of nested sources;
|
file |
diff |
annotate
|
Mon, 04 Aug 2008 17:13:34 +0200 |
wenzelm |
simplified prepare_command;
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 22:37:58 +0200 |
wenzelm |
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 17:51:42 +0200 |
wenzelm |
adapted IsarCmd.init_theory;
|
file |
diff |
annotate
|
Wed, 02 Jul 2008 16:40:17 +0200 |
wenzelm |
Toplevel.init_theory: pass name explicitly;
|
file |
diff |
annotate
|
Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
Sat, 24 May 2008 22:04:57 +0200 |
wenzelm |
added local_theory command wrappers;
|
file |
diff |
annotate
|
Wed, 14 May 2008 11:05:08 +0200 |
wenzelm |
renamed Position.path to Path.position;
|
file |
diff |
annotate
|
Thu, 17 Apr 2008 16:30:45 +0200 |
wenzelm |
Pretty.mark;
|
file |
diff |
annotate
|
Thu, 10 Apr 2008 17:01:39 +0200 |
wenzelm |
eliminated unused trace, read;
|
file |
diff |
annotate
|
Thu, 10 Apr 2008 14:53:27 +0200 |
wenzelm |
export load_thy -- no backpatching;
|
file |
diff |
annotate
|
Thu, 10 Apr 2008 13:24:15 +0200 |
wenzelm |
moved structure Isar to isar.ML;
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 14:41:19 +0100 |
wenzelm |
added process_file;
|
file |
diff |
annotate
|
Wed, 26 Mar 2008 22:40:07 +0100 |
wenzelm |
adapted to Context.thread_data interface;
|
file |
diff |
annotate
|
Tue, 18 Mar 2008 23:25:06 +0100 |
wenzelm |
theory loader: discontinued *attached* ML scripts;
|
file |
diff |
annotate
|
Sat, 15 Mar 2008 22:07:32 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|