src/Pure/Isar/token.ML
Wed, 10 Dec 2014 10:44:56 +0100 wenzelm tuned;
Tue, 09 Dec 2014 22:13:48 +0100 wenzelm imitate command markup and rendering of Isabelle/jEdit in HTML output;
Mon, 08 Dec 2014 22:42:12 +0100 wenzelm expand ML cartouches to Input.source;
Wed, 03 Dec 2014 20:45:20 +0100 wenzelm clarified define_command: send tokens more directly, without requiring keywords in ML;
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Wed, 03 Dec 2014 11:37:51 +0100 wenzelm clarified token kind;
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;
Wed, 05 Nov 2014 20:49:30 +0100 wenzelm eliminated pointless dynamic keywords (TTY legacy);
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Sat, 01 Nov 2014 19:47:48 +0100 wenzelm tuned signature (see ab2483fad861);
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Sat, 01 Nov 2014 18:46:48 +0100 wenzelm simplified -- scanning is never interactive;
Sat, 01 Nov 2014 15:01:41 +0100 wenzelm command-line terminator ";" is no longer accepted;
Fri, 31 Oct 2014 22:09:18 +0100 wenzelm removed pointless markup;
Fri, 31 Oct 2014 22:02:49 +0100 wenzelm discontinued obsolete \<^sync> marker;
Fri, 31 Oct 2014 21:10:11 +0100 wenzelm discontinued obsolete tty and prompt;
Mon, 25 Aug 2014 12:58:20 +0200 wenzelm tuned signature;
Thu, 21 Aug 2014 10:07:06 +0200 wenzelm tuned;
Wed, 20 Aug 2014 17:23:47 +0200 wenzelm support for declaration within token source;
Wed, 20 Aug 2014 11:05:41 +0200 wenzelm support for nested Token.src within Token.T;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Fri, 15 Aug 2014 18:02:34 +0200 wenzelm more informative Token.Name with history of morphisms;
Thu, 14 Aug 2014 16:20:14 +0200 wenzelm more informative Token.Fact: retain name of dynamic fact (without selection);
Tue, 18 Mar 2014 12:25:17 +0100 wenzelm more markup for improper elements;
Wed, 12 Mar 2014 16:43:17 +0100 wenzelm clarified Markup.operator vs. Markup.delimiter;
Wed, 12 Mar 2014 16:11:47 +0100 wenzelm more explicit markup for Token.Literal;
Wed, 05 Mar 2014 16:13:24 +0100 wenzelm more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
Wed, 05 Mar 2014 15:24:06 +0100 wenzelm more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
Wed, 05 Mar 2014 14:19:54 +0100 wenzelm suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
Wed, 05 Mar 2014 13:11:08 +0100 wenzelm clarified init_assignable: make double-sure that initial values are reset;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Thu, 27 Feb 2014 17:29:58 +0100 wenzelm store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
Tue, 25 Feb 2014 21:32:26 +0100 wenzelm back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
Tue, 25 Feb 2014 17:23:20 +0100 wenzelm tuned message -- more markup;
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:48:34 +0100 wenzelm clarified Token.range_of in accordance to Symbol_Pos.range;
Mon, 24 Feb 2014 10:17:29 +0100 wenzelm tuned signature;
Wed, 22 Jan 2014 16:03:11 +0100 wenzelm tuned signature;
Mon, 20 Jan 2014 20:38:51 +0100 wenzelm tuned signature;
Mon, 20 Jan 2014 20:24:44 +0100 wenzelm tuned error messages, more accurate position;
Mon, 20 Jan 2014 20:04:52 +0100 wenzelm tuned -- more direct err_prefix;
Mon, 20 Jan 2014 19:47:31 +0100 wenzelm clarified scan_cartouche_depth, according to Scala version;
Mon, 20 Jan 2014 16:56:18 +0100 wenzelm tuned errors;
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;
Tue, 19 Nov 2013 19:33:27 +0100 wenzelm maintain blobs within document state: digest + text in ML, digest-only in Scala;
Sun, 24 Feb 2013 14:11:51 +0100 wenzelm unified Command.is_proper in ML with Scala (see also 123be08eed88);
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Tue, 16 Oct 2012 20:23:00 +0200 wenzelm more proof method text position information;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Thu, 23 Aug 2012 17:46:03 +0200 wenzelm tuned messages: end-of-input rarely means physical end-of-file from the past;
Thu, 23 Aug 2012 13:55:27 +0200 wenzelm clarified type Token.file;
Mon, 20 Aug 2012 17:05:53 +0200 wenzelm some support for inlining file content into outer syntax token language;
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;
Fri, 10 Aug 2012 22:25:45 +0200 wenzelm proper error prefixes;
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, 09 Aug 2012 14:37:43 +0200 wenzelm refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
Thu, 09 Aug 2012 12:39:05 +0200 wenzelm tuned signature;
less more (0) -60 tip