src/Pure/Isar/outer_syntax.ML
Thu, 25 Aug 2011 19:12:58 +0200 wenzelm tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
Sun, 21 Aug 2011 20:42:26 +0200 wenzelm tuned Parse.group: delayed failure message;
Sat, 13 Aug 2011 20:49:41 +0200 wenzelm simplified Toplevel.init_theory: discontinued special name argument;
Sat, 13 Aug 2011 20:41:29 +0200 wenzelm simplified Toplevel.init_theory: discontinued special master argument;
Fri, 08 Jul 2011 21:44:47 +0200 wenzelm moved Outer_Syntax.load_thy to Thy_Load.load_thy;
Fri, 08 Jul 2011 20:27:09 +0200 wenzelm less stateful outer_syntax;
Fri, 01 Jul 2011 17:36:25 +0200 wenzelm clarified Thy_Syntax.element;
Sat, 26 Mar 2011 21:45:29 +0100 wenzelm present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Sat, 05 Feb 2011 20:38:32 +0100 wenzelm more tracing information via Par_List.map_name;
Thu, 13 Jan 2011 17:34:45 +0100 wenzelm Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
Sun, 09 Jan 2011 20:30:47 +0100 wenzelm more direct treatment of Position.end_offset;
Sat, 13 Nov 2010 19:21:53 +0100 wenzelm simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
Sun, 15 Aug 2010 20:19:56 +0200 wenzelm rename "unit" to "atom", to avoid confusion with the unit type;
Mon, 09 Aug 2010 18:18:32 +0200 wenzelm Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Tue, 27 Jul 2010 22:00:26 +0200 wenzelm simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
Sun, 25 Jul 2010 14:41:48 +0200 wenzelm simplified handling of theory begin/end wrt. toplevel and theory loader;
Thu, 22 Jul 2010 16:43:21 +0200 wenzelm load_thy: parallel parsing of units, which consist of statement/proof each;
Wed, 21 Jul 2010 20:32:08 +0200 wenzelm deps_thy/load_thy: store compact text to reduce space by factor 12;
Wed, 21 Jul 2010 16:14:16 +0200 wenzelm eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
Tue, 20 Jul 2010 14:44:33 +0200 wenzelm eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
Mon, 05 Jul 2010 23:07:36 +0200 wenzelm Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Mon, 17 May 2010 15:11:25 +0200 wenzelm renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
Mon, 17 May 2010 10:20:55 +0200 wenzelm centralized legacy aliases;
Sat, 15 May 2010 23:40:00 +0200 wenzelm renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Tue, 27 Oct 2009 13:16:16 +0100 wenzelm non-critical atomic accesses;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Fri, 13 Mar 2009 21:25:15 +0100 wenzelm eliminated type Args.T;
Sat, 10 Jan 2009 13:10:38 +0100 wenzelm load_thy: explicit after_load phase for presentation;
Wed, 07 Jan 2009 12:08:22 +0100 wenzelm added local_theory';
Fri, 02 Jan 2009 16:21:47 +0100 wenzelm renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
Fri, 02 Jan 2009 15:44:33 +0100 wenzelm added type 'a parser, simplified signature;
Tue, 30 Sep 2008 23:31:36 +0200 wenzelm load_thy: more precise treatment of improper cmd or proof (notably 'oops');
Tue, 30 Sep 2008 22:02:50 +0200 wenzelm load_thy: Toplevel.excursion based on units of command/proof pairs;
Tue, 30 Sep 2008 14:19:25 +0200 wenzelm simplified process_file, eliminated Toplevel.excursion;
Thu, 14 Aug 2008 19:52:37 +0200 wenzelm P.doc_source and P.ml_sorce for proper SymbolPos.text;
Wed, 13 Aug 2008 20:57:30 +0200 wenzelm load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
Tue, 12 Aug 2008 21:27:57 +0200 wenzelm Symbol.source/OuterLex.source: more explicit do_recover argument;
Mon, 11 Aug 2008 22:06:49 +0200 wenzelm Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
Thu, 07 Aug 2008 13:45:07 +0200 wenzelm updated type of nested sources;
Mon, 04 Aug 2008 17:13:34 +0200 wenzelm simplified prepare_command;
Tue, 15 Jul 2008 22:37:58 +0200 wenzelm renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
Mon, 14 Jul 2008 17:51:42 +0200 wenzelm adapted IsarCmd.init_theory;
Wed, 02 Jul 2008 16:40:17 +0200 wenzelm Toplevel.init_theory: pass name explicitly;
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Sat, 24 May 2008 22:04:57 +0200 wenzelm added local_theory command wrappers;
Wed, 14 May 2008 11:05:08 +0200 wenzelm renamed Position.path to Path.position;
Thu, 17 Apr 2008 16:30:45 +0200 wenzelm Pretty.mark;
Thu, 10 Apr 2008 17:01:39 +0200 wenzelm eliminated unused trace, read;
Thu, 10 Apr 2008 14:53:27 +0200 wenzelm export load_thy -- no backpatching;
Thu, 10 Apr 2008 13:24:15 +0200 wenzelm moved structure Isar to isar.ML;
Thu, 27 Mar 2008 14:41:19 +0100 wenzelm added process_file;
Wed, 26 Mar 2008 22:40:07 +0100 wenzelm adapted to Context.thread_data interface;
Tue, 18 Mar 2008 23:25:06 +0100 wenzelm theory loader: discontinued *attached* ML scripts;
Sat, 15 Mar 2008 22:07:32 +0100 wenzelm tuned messages;
Sat, 05 Jan 2008 21:37:21 +0100 wenzelm secure_main: removed separate welcome;
less more (0) -100 -60 tip