src/Pure/PIDE/markup.ML
Mon, 05 May 2014 15:17:07 +0200 wenzelm support print operations as asynchronous query;
Sat, 26 Apr 2014 13:07:20 +0200 wenzelm tuned signature;
Fri, 25 Apr 2014 23:42:25 +0200 wenzelm manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
Sat, 19 Apr 2014 19:52:02 +0200 wenzelm more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
Thu, 17 Apr 2014 13:21:36 +0200 wenzelm added protocol command "use_theories", with core functionality of batch build;
Sat, 12 Apr 2014 17:46:54 +0200 wenzelm markup for prose words within formal comments;
Tue, 08 Apr 2014 14:15:48 +0200 wenzelm more positions and markup;
Tue, 25 Mar 2014 16:11:00 +0100 wenzelm separate tokenization and language context for SML: no symbols, no antiquotes;
Tue, 18 Mar 2014 12:25:17 +0100 wenzelm more markup for improper elements;
Mon, 10 Mar 2014 21:15:29 +0100 wenzelm some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
Mon, 10 Mar 2014 20:27:08 +0100 wenzelm more markup;
Thu, 06 Mar 2014 16:12:26 +0100 wenzelm reject internal term names outright, and complete consts instead;
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 13:11:08 +0100 wenzelm clarified init_assignable: make double-sure that initial values are reset;
Sun, 02 Mar 2014 19:00:45 +0100 wenzelm clarified names of antiquotations and markup;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Wed, 26 Feb 2014 10:53:19 +0100 wenzelm tuned signature;
Wed, 26 Feb 2014 10:40:13 +0100 wenzelm method language markup, e.g. relevant to prevent outer keyword completion;
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:03:55 +0100 wenzelm clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
Sun, 23 Feb 2014 21:11:59 +0100 wenzelm clarified semantic completion: retain kind.full_name as official item name for history;
Sun, 23 Feb 2014 14:39:51 +0100 wenzelm clarified completion names;
Sat, 22 Feb 2014 20:52:43 +0100 wenzelm support for completion within the formal context;
Sat, 22 Feb 2014 15:07:33 +0100 wenzelm refined language context: antiquotes;
Fri, 21 Feb 2014 16:55:54 +0100 wenzelm more markup -- complete symbols within antiquotation, notably with broken arguments;
Thu, 20 Feb 2014 12:53:12 +0100 wenzelm completion of keywords and symbols based on language context;
Wed, 19 Feb 2014 20:56:29 +0100 wenzelm more markup;
Tue, 18 Feb 2014 20:50:07 +0100 wenzelm more markup;
Tue, 18 Feb 2014 18:29:02 +0100 wenzelm more standard names for protocol and markup elements;
Tue, 18 Feb 2014 17:03:12 +0100 wenzelm tuned signature;
Tue, 18 Feb 2014 16:34:02 +0100 wenzelm generic markup for embedded languages;
Mon, 17 Feb 2014 11:14:26 +0100 wenzelm more markup;
Sat, 15 Feb 2014 18:28:18 +0100 wenzelm more uniform ML keyword markup;
Sat, 18 Jan 2014 19:15:12 +0100 wenzelm support for nested text cartouches;
Mon, 09 Dec 2013 12:16:52 +0100 wenzelm added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
Tue, 03 Sep 2013 13:09:15 +0200 wenzelm cases: more position information and PIDE markup;
Sat, 17 Aug 2013 22:15:45 +0200 wenzelm some protocol to determine provers according to ML;
Fri, 02 Aug 2013 22:17:53 +0200 wenzelm more general Output.result: allow to update arbitrary properties;
Tue, 30 Jul 2013 21:22:37 +0200 wenzelm less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
Thu, 18 Jul 2013 20:53:22 +0200 wenzelm explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
Sat, 13 Jul 2013 13:25:42 +0200 wenzelm more explicit Markup.information for messages produced by "auto" tools;
Tue, 09 Jul 2013 13:17:22 +0200 wenzelm tuned protocol terminology;
Wed, 22 May 2013 14:10:45 +0200 wenzelm explicit management of Session.Protocol_Handlers, with protocol state and functions;
Tue, 14 May 2013 20:46:09 +0200 wenzelm more uniform Markup.print_real;
Tue, 14 May 2013 19:48:31 +0200 wenzelm more uniform Markup.parse_real;
Sun, 12 May 2013 20:46:17 +0200 wenzelm more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
Tue, 09 Apr 2013 21:14:00 +0200 wenzelm tuned signature;
Fri, 05 Apr 2013 20:43:43 +0200 wenzelm unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
Wed, 03 Apr 2013 21:48:43 +0200 wenzelm additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
Thu, 28 Mar 2013 15:36:45 +0100 wenzelm basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
Wed, 20 Feb 2013 15:22:22 +0100 wenzelm more tight representation of command timing;
Tue, 19 Feb 2013 13:57:13 +0100 wenzelm support for build passing timings from Scala to ML;
Tue, 19 Feb 2013 12:58:32 +0100 wenzelm support for prescient timing information within command transactions;
Tue, 19 Feb 2013 10:55:11 +0100 wenzelm emit command_timing properties into build log;
Fri, 18 Jan 2013 17:51:50 +0100 wenzelm more systematic task statistics;
Wed, 16 Jan 2013 20:41:29 +0100 wenzelm identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
Sat, 12 Jan 2013 15:00:48 +0100 wenzelm immediate theory progress for build_dialog;
Sat, 12 Jan 2013 14:47:17 +0100 wenzelm tuned signature;
Wed, 09 Jan 2013 13:38:57 +0100 wenzelm standardized treatment of timing properties;
Fri, 04 Jan 2013 12:33:25 +0100 wenzelm prefer old graph browser in Isabelle/jEdit, which still produces better layout;
less more (0) -60 tip