2010-08-15 wenzelm 2010-08-15 specific types Text.Offset and Text.Range; minor tuning;
2010-08-12 wenzelm 2010-08-12 specific Session.Commands_Changed;
2010-08-11 wenzelm 2010-08-11 consider command state as part of Snapshot, not Document;
2010-08-07 wenzelm 2010-08-07 concentrate structural document notions in document.scala; tuned;
2010-08-07 wenzelm 2010-08-07 more explicit treatment of Swing thread context; Document_Model.snapshot: require Swing thread;
2010-08-05 wenzelm 2010-08-05 Document_Model: include token marker here;
2010-08-05 wenzelm 2010-08-05 renamed to_current to convert, and from_current to revert;
2010-08-05 wenzelm 2010-08-05 Change.Snapshot: include from_current/to_current here, with precomputed changes;
2010-08-05 wenzelm 2010-08-05 explicit Change.Snapshot and Document.Node; misc tuning and clarification; Document_View: explicitly highlight outdated command status;
2010-08-05 wenzelm 2010-08-05 simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;
2010-07-19 wenzelm 2010-07-19 Session: predefined real time parameters; Document_View: delayed caret handling, for improved reactivity; selected_command: proper_command_at ignores ignored commands;
2010-07-03 wenzelm 2010-07-03 more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations; misc tuning;
2010-06-26 wenzelm 2010-06-26 simplified text_area_painter, with more precise treatment of visible line end;
2010-06-01 wenzelm 2010-06-01 basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
2010-05-30 wenzelm 2010-05-30 control tooltip font via Swing HTML, with tooltip-font-size property;
2010-05-29 wenzelm 2010-05-29 do not highlight ignored command spans; tuned;
2010-05-29 wenzelm 2010-05-29 more explicit handling of document;
2010-05-29 wenzelm 2010-05-29 explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;
2010-05-27 wenzelm 2010-05-27 indicate prospective properties;
2010-05-27 wenzelm 2010-05-27 Command.toString: include id for debugging; Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus; State.+ without side-effect on event bus; Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results; Document_View: tuned commands_changed handling and caret listening; Document_View.selected_command: proper function, not event handler state; Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);
2010-05-20 wenzelm 2010-05-20 explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
2010-05-08 wenzelm 2010-05-08 tuned headers;
2010-03-30 wenzelm 2010-03-30 adapted to Scala 2.8.0 Beta 1;
2010-01-11 wenzelm 2010-01-11 incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
2010-01-11 wenzelm 2010-01-11 more tobust treatment of Document.current_state; some timing;
2010-01-10 wenzelm 2010-01-10 eliminated Command.stop, which tends to case duplicate traversal of commands;
2010-01-10 wenzelm 2010-01-10 iterators for ranges of commands/starts -- avoid extra array per document; try/finally for saved_color; misc tuning;
2010-01-04 wenzelm 2010-01-04 slightly more uniform/robust handling of visible document; uniform changed_delay for view updates; misc tuning;
2010-01-03 wenzelm 2010-01-03 more explicit treatment of command/document state; misc tuning and clarification;
2010-01-01 wenzelm 2010-01-01 renamed current_document to recent_document (might be a bit older than current_change); Change: explicit future value of Document.Change instead of implicit lookup in Session database; Document_Model: apply Document.text_edits here (as future);
2010-01-01 wenzelm 2010-01-01 renamed Proof_Document to Document;
2009-12-29 wenzelm 2009-12-29 tuned;
2009-12-29 wenzelm 2009-12-29 tuned caret_listener/selected_command;
2009-12-29 wenzelm 2009-12-29 eliminated global Session.document_0 -- did not work due to hardwired id; more precise Session.begin_document, avoid race on var prover; replaced slightly odd Session.document_versions by Sassion.documents table (cf. src/Pure/Isar/isar_document.ML); simplified edit_document in ML: initial empty command is identified by ""; misc tuning;
2009-12-29 wenzelm 2009-12-29 tuned;
2009-12-18 wenzelm 2009-12-18 imitate PG 4 colors;
2009-12-15 wenzelm 2009-12-15 some explicit Swing_Thread guards;
2009-12-15 wenzelm 2009-12-15 direct apply for Document_Model and Document_View;
2009-12-15 wenzelm 2009-12-15 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea); incorporate Document_Overview into Document_View; eliminated Plugin.mapping in favour of direct association via generic properties; support several views per model; misc tuning;