2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 tuned signature -- eliminated pointless type synonym;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-07-04 wenzelm 2013-07-04 tuned;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-03-23 wenzelm 2013-03-23 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 wenzelm 2013-03-23 structural equality for Command.Results; more general Command.State.eq_content;
2013-01-25 wenzelm 2013-01-25 clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally; reverted f3588e59aeaa accordingly;
2012-12-14 wenzelm 2012-12-14 tuned;
2012-12-14 wenzelm 2012-12-14 tuned implementation according to Library.insert/merge in ML;
2012-12-14 wenzelm 2012-12-14 more formal class Command.Results;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
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-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 wenzelm 2012-11-22 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;
2012-11-21 wenzelm 2012-11-21 always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;
2012-09-28 wenzelm 2012-09-28 tuned signature;
2012-09-27 wenzelm 2012-09-27 operations to turn markup into XML; tuned;
2012-09-22 wenzelm 2012-09-22 accumulate under exec_id as well;
2012-09-22 wenzelm 2012-09-22 more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);
2012-09-21 wenzelm 2012-09-21 more realistic sendback: pick exec_id from message position and text from buffer;
2012-09-20 wenzelm 2012-09-20 tuned signature;
2012-09-19 wenzelm 2012-09-19 earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
2012-09-18 wenzelm 2012-09-18 more explicit message markup and rendering;
2012-09-18 wenzelm 2012-09-18 some actual rich text markup via XML.content_markup; tuned signature;
2012-09-18 wenzelm 2012-09-18 some support for inital command markup; tuned signature;
2012-09-14 wenzelm 2012-09-14 refined output panel: more value-oriented approach to update and caret focus;
2012-08-31 wenzelm 2012-08-31 more markup for failed goal forks, reusing "bad";
2012-08-24 wenzelm 2012-08-24 more precise counting of line/column;
2012-08-10 wenzelm 2012-08-10 clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;
2012-08-09 wenzelm 2012-08-09 tuned signature;
2012-08-07 wenzelm 2012-08-07 more structural parsing for minor modes; tuned signatures;
2012-07-30 wenzelm 2012-07-30 tuned signature;
2012-04-13 wenzelm 2012-04-13 include trailing comments in proper_command range;
2012-03-19 wenzelm 2012-03-19 clarified command span classification: strict Command.is_command, permissive;
2012-03-13 wenzelm 2012-03-13 clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-04 wenzelm 2012-03-04 added Command.proper_range (still unused);
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-01-09 wenzelm 2012-01-09 tuned;
2012-01-07 wenzelm 2012-01-07 accumulate status as regular markup for command range; tuned signature;
2011-12-01 wenzelm 2011-12-01 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
2011-11-29 wenzelm 2011-11-29 clarified modules;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-26 wenzelm 2011-11-26 sharing of token source with span source;
2011-11-11 wenzelm 2011-11-11 prefer statically typed Text.Markup;
2011-09-17 wenzelm 2011-09-17 Document.Node.Name convenience;
2011-09-01 wenzelm 2011-09-01 more abstract Document.Node.Name; tuned signature;
2011-08-31 wenzelm 2011-08-31 maintain name of *the* enclosing node as part of command -- avoid full document traversal;
2011-08-25 wenzelm 2011-08-25 slightly more abstract Command.Perspective;
2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-07-04 wenzelm 2011-07-04 Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-06-23 wenzelm 2011-06-23 explicit import java.lang.System to prevent odd scope problems;
2010-11-16 wenzelm 2010-11-16 avoid spam;
2010-11-10 wenzelm 2010-11-10 some support for nested source structure, based on section headings;