src/Pure/PIDE/markup.ML
2015-12-17 wenzelm 2015-12-17 support pretty break indent, like underlying ML systems;
2015-11-13 wenzelm 2015-11-13 added antiquotation @{doc}, e.g. useful for demonstration purposes;
2015-11-10 wenzelm 2015-11-10 added document antiquotation @{theory_text}; tuned document;
2015-11-07 wenzelm 2015-11-07 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
2015-11-07 wenzelm 2015-11-07 less confusing markup;
2015-11-02 wenzelm 2015-11-02 clarified completion of Isabelle symbols within document source;
2015-10-15 wenzelm 2015-10-15 report Markdown document structure;
2015-09-21 wenzelm 2015-09-21 tuned signature;
2015-08-05 wenzelm 2015-08-05 protocol support for thread debugger state;
2015-07-30 wenzelm 2015-07-30 maintain debugger output messages;
2015-07-29 wenzelm 2015-07-29 separate channel for debugger output; clarified thread name;
2015-07-17 wenzelm 2015-07-17 report possible breakpoint positions;
2015-04-06 wenzelm 2015-04-06 clarified command keyword markup;
2015-03-24 wenzelm 2015-03-24 clarified input source;
2015-01-15 wenzelm 2015-01-15 more informative build_theories_result: cumulative Runtime.exn_message;
2015-01-14 wenzelm 2015-01-14 clarified build_theories;
2014-12-30 wenzelm 2014-12-30 explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-12-10 wenzelm 2014-12-10 more explicit markup for improper commands; clarified CSS rendering;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-12-03 wenzelm 2014-12-03 clarified token kind;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-10-31 wenzelm 2014-10-31 removed pointless markup; tuned comments;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete tty and prompt;
2014-10-05 wenzelm 2014-10-05 citation tooltip/hyperlink based on open buffers with .bib files;
2014-10-05 wenzelm 2014-10-05 bibtex support in ML: document antiquotation @{cite} with markup;
2014-09-26 wenzelm 2014-09-26 support for sub-expression markup;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-15 wenzelm 2014-08-15 explicit system message for protocol failure -- show on Syslog panel instead of Raw Output; more robust crash recovery: warning could crash again;
2014-07-21 wenzelm 2014-07-21 regular message to refer to Simplifier Trace panel (unused);
2014-05-05 wenzelm 2014-05-05 support print operations as asynchronous query;
2014-04-26 wenzelm 2014-04-26 tuned signature;
2014-04-25 wenzelm 2014-04-25 manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
2014-04-19 wenzelm 2014-04-19 more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
2014-04-17 wenzelm 2014-04-17 added protocol command "use_theories", with core functionality of batch build;
2014-04-12 wenzelm 2014-04-12 markup for prose words within formal comments;
2014-04-08 wenzelm 2014-04-08 more positions and markup;
2014-03-25 wenzelm 2014-03-25 separate tokenization and language context for SML: no symbols, no antiquotes;
2014-03-18 wenzelm 2014-03-18 more markup for improper elements;
2014-03-10 wenzelm 2014-03-10 some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-03-10 wenzelm 2014-03-10 more markup;
2014-03-06 wenzelm 2014-03-06 reject internal term names outright, and complete consts instead; more general Name_Space.check_reports; more compact Markup.markup_report;
2014-03-05 wenzelm 2014-03-05 more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
2014-03-05 wenzelm 2014-03-05 clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
2014-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-26 wenzelm 2014-02-26 tuned signature;
2014-02-26 wenzelm 2014-02-26 method language markup, e.g. relevant to prevent outer keyword completion;
2014-02-25 wenzelm 2014-02-25 back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;
2014-02-25 wenzelm 2014-02-25 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind; tuned message;
2014-02-23 wenzelm 2014-02-23 clarified semantic completion: retain kind.full_name as official item name for history; misc tuning;
2014-02-23 wenzelm 2014-02-23 clarified completion names; tuned signature;
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2014-02-22 wenzelm 2014-02-22 refined language context: antiquotes; support default completions, with move of caret position; tuned signature;
2014-02-21 wenzelm 2014-02-21 more markup -- complete symbols within antiquotation, notably with broken arguments;
2014-02-20 wenzelm 2014-02-20 completion of keywords and symbols based on language context;
2014-02-19 wenzelm 2014-02-19 more markup; clarified token range;
2014-02-18 wenzelm 2014-02-18 more markup;
2014-02-18 wenzelm 2014-02-18 more standard names for protocol and markup elements;
2014-02-18 wenzelm 2014-02-18 tuned signature;