src/Pure/Isar/outer_syntax.ML
Mon, 25 Feb 2013 12:17:11 +0100 wenzelm tuned comment;
Sun, 24 Feb 2013 17:29:55 +0100 wenzelm simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
Wed, 20 Feb 2013 00:00:42 +0100 wenzelm support nested Thy_Syntax.element;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Mon, 26 Nov 2012 16:16:47 +0100 wenzelm more general sendback properties;
Mon, 26 Nov 2012 13:54:43 +0100 wenzelm refined outer syntax 'help' command;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Tue, 25 Sep 2012 18:24:49 +0200 wenzelm tuned;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Fri, 24 Aug 2012 12:35:39 +0200 wenzelm check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
Mon, 20 Aug 2012 14:09:09 +0200 wenzelm added keyword kind "thy_load" (with optional list of file extensions);
Sat, 11 Aug 2012 18:05:41 +0200 wenzelm clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
Sat, 11 Aug 2012 17:24:21 +0200 wenzelm clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
Thu, 09 Aug 2012 22:31:04 +0200 wenzelm some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
Thu, 02 Aug 2012 13:37:58 +0200 wenzelm report commands as formal entities, with def/ref positions;
Thu, 02 Aug 2012 12:36:54 +0200 wenzelm more official command specifications, including source position;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
Thu, 05 Jul 2012 15:40:57 +0200 wenzelm internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
Tue, 10 Apr 2012 21:31:05 +0200 wenzelm static relevance of proof via syntax keywords;
Mon, 19 Mar 2012 18:18:42 +0100 wenzelm allow keyword tags to be redefined, but not the command category;
Fri, 16 Mar 2012 21:40:21 +0100 wenzelm check declared vs. defined commands at end of session;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Fri, 16 Mar 2012 13:05:30 +0100 wenzelm define keywords early when processing the theory header, before running the body commands;
Fri, 16 Mar 2012 11:26:55 +0100 wenzelm clarified Keyword.is_keyword: union of minor and major;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Mon, 12 Mar 2012 17:27:52 +0100 wenzelm refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
Tue, 06 Sep 2011 20:37:07 +0200 wenzelm bulk reports for improved message throughput;
Fri, 02 Sep 2011 20:35:32 +0200 wenzelm tuned;
Fri, 02 Sep 2011 20:29:39 +0200 wenzelm more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
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;
less more (0) -100 -60 tip