src/Pure/PIDE/markup.ML
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;
2014-02-18 wenzelm 2014-02-18 generic markup for embedded languages;
2014-02-17 wenzelm 2014-02-17 more markup;
2014-02-15 wenzelm 2014-02-15 more uniform ML keyword markup; tuned;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-12-09 wenzelm 2013-12-09 added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-09-03 wenzelm 2013-09-03 cases: more position information and PIDE markup;
2013-08-17 wenzelm 2013-08-17 some protocol to determine provers according to ML;
2013-08-02 wenzelm 2013-08-02 more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);
2013-07-30 wenzelm 2013-07-30 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace; propagate flush from ML to Scala via special protocol message; more formal type Message_Channel.message;
2013-07-18 wenzelm 2013-07-18 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
2013-07-13 wenzelm 2013-07-13 more explicit Markup.information for messages produced by "auto" tools;
2013-07-09 wenzelm 2013-07-09 tuned protocol terminology; tuned signature;
2013-05-22 wenzelm 2013-05-22 explicit management of Session.Protocol_Handlers, with protocol state and functions; more self-contained ML/Scala module Invoke_Scala;
2013-05-14 wenzelm 2013-05-14 more uniform Markup.print_real;
2013-05-14 wenzelm 2013-05-14 more uniform Markup.parse_real;
2013-05-12 wenzelm 2013-05-12 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
2013-04-09 wenzelm 2013-04-09 tuned signature;
2013-04-05 wenzelm 2013-04-05 unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
2013-04-03 wenzelm 2013-04-03 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-03-28 wenzelm 2013-03-28 basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
2013-02-20 wenzelm 2013-02-20 more tight representation of command timing; tuned signatures; tuned;
2013-02-19 wenzelm 2013-02-19 support for build passing timings from Scala to ML;
2013-02-19 wenzelm 2013-02-19 support for prescient timing information within command transactions;
2013-02-19 wenzelm 2013-02-19 emit command_timing properties into build log; tuned;
2013-01-18 wenzelm 2013-01-18 more systematic task statistics;
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-12 wenzelm 2013-01-12 immediate theory progress for build_dialog; more formal Bash_Result -- accumulate output as lines;
2013-01-12 wenzelm 2013-01-12 tuned signature;
2013-01-09 wenzelm 2013-01-09 standardized treatment of timing properties;
2013-01-04 wenzelm 2013-01-04 prefer old graph browser in Isabelle/jEdit, which still produces better layout; clarified print mode "active_graph": allow to switch "browser" vs. "graphview" uniformly; tuned signature;
2013-01-02 wenzelm 2013-01-02 inline ML statistics into build log;
2012-12-15 wenzelm 2012-12-15 explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
2012-12-15 wenzelm 2012-12-15 fold main goal;
2012-12-14 wenzelm 2012-12-14 more subgoal markup information, which is potentially useful to manage proof state output;
2012-12-13 wenzelm 2012-12-13 enable Isabelle/ML to produce uninterpreted result messages as well;
2012-12-13 wenzelm 2012-12-13 identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
2012-12-12 wenzelm 2012-12-12 rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
2012-12-12 wenzelm 2012-12-12 support dialog via document content;
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;