src/Pure/Thy/thy_syntax.ML
Fri, 09 Oct 2015 21:16:00 +0200 wenzelm more direct HTML presentation, without print mode;
Wed, 25 Mar 2015 11:39:52 +0100 wenzelm tuned signature;
Wed, 10 Dec 2014 13:45:44 +0100 wenzelm more explicit markup for improper commands;
Tue, 09 Dec 2014 22:13:48 +0100 wenzelm imitate command markup and rendering of Isabelle/jEdit in HTML output;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source;
Thu, 06 Nov 2014 15:47:04 +0100 wenzelm more explicit Keyword.keywords;
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Tue, 12 Aug 2014 00:08:32 +0200 wenzelm separate module Command_Span: mostly syntactic representation;
Mon, 11 Aug 2014 22:46:27 +0200 wenzelm clarified Command_Span in accordance to Scala (see also c2c1e5944536);
Mon, 11 Aug 2014 22:29:48 +0200 wenzelm more explicit type Span in Scala, according to ML version;
Wed, 28 May 2014 16:16:40 +0200 wenzelm tuned signature;
Wed, 05 Mar 2014 14:19:54 +0100 wenzelm suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Tue, 25 Feb 2014 17:03:55 +0100 wenzelm clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
Mon, 24 Feb 2014 10:17:29 +0100 wenzelm tuned signature;
Wed, 22 Jan 2014 21:33:50 +0100 wenzelm clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Tue, 19 Nov 2013 19:43:26 +0100 wenzelm release file errors at runtime: Command.eval instead of Command.read;
Sat, 16 Nov 2013 18:08:57 +0100 wenzelm tuned signature;
Tue, 24 Sep 2013 16:06:12 +0200 wenzelm clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer);
Wed, 13 Mar 2013 21:25:08 +0100 wenzelm clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
Sun, 03 Mar 2013 13:23:06 +0100 wenzelm more Thy_Syntax.element operations;
Sun, 24 Feb 2013 17:29:55 +0100 wenzelm simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
Sun, 24 Feb 2013 14:14:07 +0100 wenzelm tuned;
Wed, 20 Feb 2013 00:00:42 +0100 wenzelm support nested Thy_Syntax.element;
Mon, 26 Nov 2012 21:10:42 +0100 wenzelm more uniform Symbol.is_ascii_identifier in ML/Scala;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Wed, 22 Aug 2012 11:56:13 +0200 wenzelm tuned errors;
Mon, 20 Aug 2012 17:05:53 +0200 wenzelm some support for inlining file content into outer syntax token language;
less more (0) -50 -30 tip