2010-08-14 wenzelm 2010-08-14 Keyword.status: always suppress position;
2010-08-14 wenzelm 2010-08-14 moved Document.text_edits to Thy_Syntax;
2010-08-14 wenzelm 2010-08-14 tuned;
2010-08-13 wenzelm 2010-08-13 explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here;
2010-08-12 wenzelm 2010-08-12 simplified/clarified Change: transition prev --edits--> result, based on futures; Session.history: plain List instead of somewhat indirect Change.ancestors; tuned;
2010-08-12 wenzelm 2010-08-12 moved snapshot to Session (cf. 96b22dfeb56a);
2010-08-12 wenzelm 2010-08-12 Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway; Document.edit_text: create new document id here;
2010-08-12 wenzelm 2010-08-12 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type (ML) / Document.ID;
2010-08-12 wenzelm 2010-08-12 specific Session.Commands_Changed;
2010-08-12 wenzelm 2010-08-12 consider snapshot as service of Session, not Document.Change;
2010-08-11 wenzelm 2010-08-11 represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
2010-08-10 wenzelm 2010-08-10 edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
2010-08-07 wenzelm 2010-08-07 simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; XML.cache_tree: actually store XML.Text as well; added;
2010-08-07 wenzelm 2010-08-07 concentrate structural document notions in document.scala; tuned;
2010-08-07 wenzelm 2010-08-07 maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
2010-08-07 wenzelm 2010-08-07 replaced individual Document_Model history by all-inclusive one in Session; Document_Model: provide thy_name externally, i.e. by central Isabelle plugin; tuned;
2010-08-07 wenzelm 2010-08-07 misc tuning and clarification;
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-04 wenzelm 2010-07-04 simplified Isabelle_Process.Result: use markup directly;
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-22 wenzelm 2010-05-22 separate event bus and dockable for raw output (stdout);
2010-05-22 wenzelm 2010-05-22 ignore system messages;
2010-05-21 wenzelm 2010-05-21 bad_result: report fully explicit message;
2010-05-15 wenzelm 2010-05-15 renamed Outer_Keyword to Keyword (in Scala);
2010-05-10 wenzelm 2010-05-10 ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
2010-05-06 wenzelm 2010-05-06 extractors for document updates; Session.handle_result: use extractors instead of raw patterns -- NB: using mixed patterns of case classes vs. extractors crashes Scala 2.8.1 RC1;
2010-05-05 wenzelm 2010-05-05 some rearrangement of Scala sources;
2010-02-06 wenzelm 2010-02-06 fixed spelling;
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);