| Wed, 03 Jul 2013 16:58:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 03 Jul 2013 16:19:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2013 20:54:55 +0200 |
wenzelm |
tuned signature -- agree with markup terminology;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:11 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sun, 24 Feb 2013 17:29:55 +0100 |
wenzelm |
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 00:00:42 +0100 |
wenzelm |
support nested Thy_Syntax.element;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 13:54:43 +0100 |
wenzelm |
refined outer syntax 'help' command;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 18:24:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
| Mon, 20 Aug 2012 14:09:09 +0200 |
wenzelm |
added keyword kind "thy_load" (with optional list of file extensions);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 17:24:21 +0200 |
wenzelm |
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 13:37:58 +0200 |
wenzelm |
report commands as formal entities, with def/ref positions;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 12:36:54 +0200 |
wenzelm |
more official command specifications, including source position;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 10 Apr 2012 21:31:05 +0200 |
wenzelm |
static relevance of proof via syntax keywords;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 18:18:42 +0100 |
wenzelm |
allow keyword tags to be redefined, but not the command category;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 21:40:21 +0100 |
wenzelm |
check declared vs. defined commands at end of session;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 11:26:55 +0100 |
wenzelm |
clarified Keyword.is_keyword: union of minor and major;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 20:37:07 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 20:35:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 20:29:39 +0200 |
wenzelm |
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 20:42:26 +0200 |
wenzelm |
tuned Parse.group: delayed failure message;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:49:41 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special name argument;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 21:44:47 +0200 |
wenzelm |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 20:27:09 +0200 |
wenzelm |
less stateful outer_syntax;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 17:36:25 +0200 |
wenzelm |
clarified Thy_Syntax.element;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Sat, 05 Feb 2011 20:38:32 +0100 |
wenzelm |
more tracing information via Par_List.map_name;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 17:34:45 +0100 |
wenzelm |
Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 20:30:47 +0100 |
wenzelm |
more direct treatment of Position.end_offset;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 19:21:53 +0100 |
wenzelm |
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
|
file |
diff |
annotate
|
| Sun, 15 Aug 2010 20:19:56 +0200 |
wenzelm |
rename "unit" to "atom", to avoid confusion with the unit type;
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 18:18:32 +0200 |
wenzelm |
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 25 Jul 2010 14:41:48 +0200 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 16:43:21 +0200 |
wenzelm |
load_thy: parallel parsing of units, which consist of statement/proof each;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 20:32:08 +0200 |
wenzelm |
deps_thy/load_thy: store compact text to reduce space by factor 12;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 16:14:16 +0200 |
wenzelm |
eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 23:07:36 +0200 |
wenzelm |
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 10:20:55 +0200 |
wenzelm |
centralized legacy aliases;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 13:16:16 +0100 |
wenzelm |
non-critical atomic accesses;
|
file |
diff |
annotate
|
| 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
|
| Sat, 05 Jan 2008 21:37:21 +0100 |
wenzelm |
secure_main: removed separate welcome;
|
file |
diff |
annotate
|
| Tue, 01 Jan 2008 16:09:28 +0100 |
wenzelm |
try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 23:26:27 +0100 |
wenzelm |
cond_timeit: added message argument;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2007 21:20:06 +0100 |
wenzelm |
secure_main: enforces terminator, to gain robustness;
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 22:19:53 +0100 |
wenzelm |
added off-line parse;
|
file |
diff |
annotate
|
| Tue, 04 Dec 2007 22:49:27 +0100 |
wenzelm |
added Isar.secure_main;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 17:46:52 +0200 |
wenzelm |
report on keyword/command declarations;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:08 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2007 23:07:47 +0200 |
wenzelm |
load_thy: try_ml_file unconditionally;
|
file |
diff |
annotate
|
| Mon, 30 Jul 2007 11:12:28 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 22:41:58 +0200 |
wenzelm |
load_thy: avoid reloading of text;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:46 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 17:54:15 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:52 +0200 |
wenzelm |
moved deps_thy to ThyLoad (independent of outer syntax);
|
file |
diff |
annotate
|
| Thu, 12 Jul 2007 00:15:34 +0200 |
wenzelm |
exported command_keyword;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 23:29:47 +0200 |
wenzelm |
export get_lexicons;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 00:17:52 +0200 |
wenzelm |
nested source: explicit interactive flag for recover avoids duplicate errors;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 23:12:46 +0200 |
wenzelm |
toplevel_source: interactive flag indicates intermittent error_msg;
|
file |
diff |
annotate
|
| Mon, 30 Apr 2007 13:32:58 +0200 |
wenzelm |
explicit treatment of legacy_features;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:29 +0100 |
wenzelm |
renamed IsarOutput to ThyOutput;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 13:09:33 +0100 |
wenzelm |
adapted ML context operations;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:07 +0100 |
wenzelm |
refrain from setting ml_prompts again;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 12:33:27 +0100 |
wenzelm |
Toplevel.init_state;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 22:38:30 +0100 |
wenzelm |
prefer Proof.context over Context.generic;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:19:52 +0100 |
wenzelm |
added Isar.goal;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:46:49 +0100 |
wenzelm |
Isar.context: proper error;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:03:10 +0200 |
wenzelm |
removed OldGoals.legacy flag (always warn);
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 15:21:33 +0200 |
wenzelm |
added Isar.context;
|
file |
diff |
annotate
|