Tue, 31 Jul 2018 21:21:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 31 Jul 2018 21:11:24 +0200 |
wenzelm |
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
|
file |
diff |
annotate
|
Sun, 27 May 2018 13:42:01 +0200 |
wenzelm |
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
|
file |
diff |
annotate
|
Mon, 14 May 2018 22:01:00 +0200 |
wenzelm |
adjust position according to offset of command/exec id;
|
file |
diff |
annotate
|
Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 25 Jan 2018 11:29:52 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 25 Jan 2018 11:20:31 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
Wed, 24 Jan 2018 20:47:36 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
Wed, 24 Jan 2018 20:08:33 +0100 |
wenzelm |
tuned signature: removed unused operations;
|
file |
diff |
annotate
|
Wed, 24 Jan 2018 16:34:24 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Wed, 24 Jan 2018 11:56:38 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
Tue, 16 Jan 2018 11:27:52 +0100 |
wenzelm |
discontinued old form of marginal comments;
|
file |
diff |
annotate
|
Mon, 15 Jan 2018 23:03:01 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
Mon, 15 Jan 2018 22:46:04 +0100 |
wenzelm |
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
|
file |
diff |
annotate
|
Mon, 12 Jun 2017 11:32:23 +0200 |
wenzelm |
more markup for HTML rendering;
|
file |
diff |
annotate
|
Mon, 12 Jun 2017 10:58:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 08 Jun 2017 23:04:07 +0200 |
wenzelm |
more HTML rendering as in Isabelle/jEdit;
|
file |
diff |
annotate
|
Fri, 10 Mar 2017 17:08:21 +0100 |
wenzelm |
avoid extra decorations for regular command keywords;
|
file |
diff |
annotate
|
Wed, 28 Dec 2016 10:39:50 +0100 |
wenzelm |
more uniform treatment of "bad" like other messages (with serial number);
|
file |
diff |
annotate
|
Thu, 27 Oct 2016 21:52:12 +0200 |
wenzelm |
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
|
file |
diff |
annotate
|
Thu, 22 Sep 2016 11:25:27 +0200 |
wenzelm |
discontinued raw symbols;
|
file |
diff |
annotate
|
Tue, 09 Aug 2016 19:44:28 +0200 |
wenzelm |
print name in parsable form;
|
file |
diff |
annotate
|
Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
Fri, 01 Apr 2016 17:56:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 01 Apr 2016 17:49:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 01 Apr 2016 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 31 Mar 2016 16:23:25 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Thu, 07 Jan 2016 16:10:13 +0100 |
wenzelm |
prefer non-ASCII output;
|
file |
diff |
annotate
|
Thu, 10 Dec 2015 15:53:28 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 21:20:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 21:10:45 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 20:58:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
Tue, 10 Nov 2015 19:03:29 +0100 |
wenzelm |
added document antiquotation @{theory_text};
|
file |
diff |
annotate
|
Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 18 Oct 2015 17:24:24 +0200 |
wenzelm |
support control symbol antiquotations;
|
file |
diff |
annotate
|
Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
Wed, 02 Sep 2015 13:26:29 +0200 |
wenzelm |
trim context more thoroughly;
|
file |
diff |
annotate
|
Fri, 01 May 2015 13:58:06 +0200 |
wenzelm |
modifier markup for all parsed tokens;
|
file |
diff |
annotate
|
Thu, 09 Apr 2015 20:42:32 +0200 |
wenzelm |
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
|
file |
diff |
annotate
|
Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
Sat, 04 Apr 2015 21:21:40 +0200 |
wenzelm |
more general notion of command span: command keyword not necessarily at start;
|
file |
diff |
annotate
|
Thu, 02 Apr 2015 20:07:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 02 Apr 2015 12:24:30 +0200 |
wenzelm |
operation on embedded sources for Eisbach;
|
file |
diff |
annotate
|
Thu, 02 Apr 2015 11:28:59 +0200 |
wenzelm |
tuned -- emphasize semantics of already checked src;
|
file |
diff |
annotate
|
Wed, 25 Mar 2015 11:39:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|
Tue, 10 Mar 2015 13:55:10 +0100 |
wenzelm |
clarified Token.check_src: intern at most once;
|
file |
diff |
annotate
|
Sat, 07 Mar 2015 15:40:36 +0100 |
wenzelm |
added declare_maxidx operations for Eisbach;
|
file |
diff |
annotate
|
Wed, 10 Dec 2014 13:45:44 +0100 |
wenzelm |
more explicit markup for improper commands;
|
file |
diff |
annotate
|
Wed, 10 Dec 2014 10:44:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 09 Dec 2014 22:13:48 +0100 |
wenzelm |
imitate command markup and rendering of Isabelle/jEdit in HTML output;
|
file |
diff |
annotate
|
Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
Wed, 03 Dec 2014 20:45:20 +0100 |
wenzelm |
clarified define_command: send tokens more directly, without requiring keywords in ML;
|
file |
diff |
annotate
|
Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 03 Dec 2014 11:37:51 +0100 |
wenzelm |
clarified token kind;
|
file |
diff |
annotate
|
Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
Wed, 05 Nov 2014 20:49:30 +0100 |
wenzelm |
eliminated pointless dynamic keywords (TTY legacy);
|
file |
diff |
annotate
|
Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
Sat, 01 Nov 2014 19:47:48 +0100 |
wenzelm |
tuned signature (see ab2483fad861);
|
file |
diff |
annotate
|
Sat, 01 Nov 2014 19:33:51 +0100 |
wenzelm |
recover via scanner;
|
file |
diff |
annotate
|
Sat, 01 Nov 2014 18:46:48 +0100 |
wenzelm |
simplified -- scanning is never interactive;
|
file |
diff |
annotate
|
Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 22:09:18 +0100 |
wenzelm |
removed pointless markup;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 21:10:11 +0100 |
wenzelm |
discontinued obsolete tty and prompt;
|
file |
diff |
annotate
|
Mon, 25 Aug 2014 12:58:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 21 Aug 2014 10:07:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 20 Aug 2014 17:23:47 +0200 |
wenzelm |
support for declaration within token source;
|
file |
diff |
annotate
|
Wed, 20 Aug 2014 11:05:41 +0200 |
wenzelm |
support for nested Token.src within Token.T;
|
file |
diff |
annotate
|
Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
Fri, 15 Aug 2014 18:02:34 +0200 |
wenzelm |
more informative Token.Name with history of morphisms;
|
file |
diff |
annotate
|
Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
Tue, 18 Mar 2014 12:25:17 +0100 |
wenzelm |
more markup for improper elements;
|
file |
diff |
annotate
|
Wed, 12 Mar 2014 16:43:17 +0100 |
wenzelm |
clarified Markup.operator vs. Markup.delimiter;
|
file |
diff |
annotate
|
Wed, 12 Mar 2014 16:11:47 +0100 |
wenzelm |
more explicit markup for Token.Literal;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 15:24:06 +0100 |
wenzelm |
more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 14:19:54 +0100 |
wenzelm |
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
|
file |
diff |
annotate
|
Wed, 05 Mar 2014 13:11:08 +0100 |
wenzelm |
clarified init_assignable: make double-sure that initial values are reset;
|
file |
diff |
annotate
|
Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 25 Feb 2014 17:23:20 +0100 |
wenzelm |
tuned message -- more markup;
|
file |
diff |
annotate
|
Tue, 25 Feb 2014 17:03:55 +0100 |
wenzelm |
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
|
file |
diff |
annotate
|
Mon, 24 Feb 2014 10:48:34 +0100 |
wenzelm |
clarified Token.range_of in accordance to Symbol_Pos.range;
|
file |
diff |
annotate
|
Mon, 24 Feb 2014 10:17:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 22 Jan 2014 16:03:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 20:38:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 20:24:44 +0100 |
wenzelm |
tuned error messages, more accurate position;
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 20:04:52 +0100 |
wenzelm |
tuned -- more direct err_prefix;
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 19:47:31 +0100 |
wenzelm |
clarified scan_cartouche_depth, according to Scala version;
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 16:56:18 +0100 |
wenzelm |
tuned errors;
|
file |
diff |
annotate
|
Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 19:43:26 +0100 |
wenzelm |
release file errors at runtime: Command.eval instead of Command.read;
|
file |
diff |
annotate
|
Tue, 19 Nov 2013 19:33:27 +0100 |
wenzelm |
maintain blobs within document state: digest + text in ML, digest-only in Scala;
|
file |
diff |
annotate
|
Sun, 24 Feb 2013 14:11:51 +0100 |
wenzelm |
unified Command.is_proper in ML with Scala (see also 123be08eed88);
|
file |
diff |
annotate
|
Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
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, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
Thu, 23 Aug 2012 17:46:03 +0200 |
wenzelm |
tuned messages: end-of-input rarely means physical end-of-file from the past;
|
file |
diff |
annotate
|
Thu, 23 Aug 2012 13:55:27 +0200 |
wenzelm |
clarified type Token.file;
|
file |
diff |
annotate
|
Mon, 20 Aug 2012 17:05:53 +0200 |
wenzelm |
some support for inlining file content into outer syntax token language;
|
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
|
Fri, 10 Aug 2012 22:25:45 +0200 |
wenzelm |
proper error prefixes;
|
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, 09 Aug 2012 14:37:43 +0200 |
wenzelm |
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
|
file |
diff |
annotate
|
Thu, 09 Aug 2012 12:39:05 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 04 Mar 2012 16:02:14 +0100 |
wenzelm |
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
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
|
Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 14:33:08 +0200 |
wenzelm |
more precise Symbol_Pos.quote_string;
|
file |
diff |
annotate
|
Sun, 10 Jul 2011 20:59:04 +0200 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file |
diff |
annotate
|
Fri, 08 Jul 2011 16:13:34 +0200 |
wenzelm |
discontinued special treatment of hard tabulators;
|
file |
diff |
annotate
|
Sat, 30 Apr 2011 18:16:40 +0200 |
wenzelm |
more uniform variations of scan_string;
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|