src/Pure/System/session.scala
2010-11-11 wenzelm 2010-11-11 unified type Document.Edit;
2010-11-11 wenzelm 2010-11-11 replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character); tuned;
2010-09-25 wenzelm 2010-09-25 simplified / clarified Session.Phase;
2010-09-25 wenzelm 2010-09-25 tuned signature;
2010-09-24 wenzelm 2010-09-24 more informative Session.Phase;
2010-09-23 wenzelm 2010-09-23 simplified Session.Phase; slightly more robust session startup; misc tuning;
2010-09-23 wenzelm 2010-09-23 explicit Session.Phase indication with associated event bus; asynchronous Session.start(); synchronous Session.stop(); added Plugin.session_manager on top of basic Session; eliminated separate isabelle.activate action; misc tuning;
2010-09-23 wenzelm 2010-09-23 tuned signature;
2010-09-23 wenzelm 2010-09-23 manage persistent syslog via Session, not Isabelle_Process; tuned;
2010-09-23 wenzelm 2010-09-23 tuned prover message categorization;
2010-09-22 wenzelm 2010-09-22 basic setup for Session_Dockable controls;
2010-09-22 wenzelm 2010-09-22 Session_Dockable: basic syslog output;
2010-09-22 wenzelm 2010-09-22 just one Session.raw_messages event bus;
2010-09-22 wenzelm 2010-09-22 main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;
2010-09-20 wenzelm 2010-09-20 added Isabelle_Process.syslog; refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads; tuned;
2010-09-19 wenzelm 2010-09-19 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop; tuned;
2010-09-19 wenzelm 2010-09-19 simplified Isabelle_Process message kinds; misc tuning and simplification;
2010-09-18 wenzelm 2010-09-18 recovered basic session stop/restart;
2010-08-31 wenzelm 2010-08-31 Document state assignment indicates command change;
2010-08-29 wenzelm 2010-08-29 session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
2010-08-29 wenzelm 2010-08-29 session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
2010-08-29 wenzelm 2010-08-29 use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled; clarified session signalling;
2010-08-28 wenzelm 2010-08-28 avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;
2010-08-28 wenzelm 2010-08-28 include Document.History in Document.State -- just one universal session state maintained by main actor; Session.command_change_buffer: thread actor ensures asynchronous dispatch; misc tuning;
2010-08-25 wenzelm 2010-08-25 organized markup properties via apply/unapply patterns;
2010-08-23 wenzelm 2010-08-23 main session actor as independent thread, to avoid starvation via regular worker pool; tuned;
2010-08-20 wenzelm 2010-08-20 tuned signatures;
2010-08-16 wenzelm 2010-08-16 XML.Cache: pipe-lined (thread-safe) version using actor; tuned Isabelle_Process.pid handling;
2010-08-15 wenzelm 2010-08-15 moved Text_Edit to Text.Edit; tuned;
2010-08-15 wenzelm 2010-08-15 moved History/Snapshot to document.scala;
2010-08-15 wenzelm 2010-08-15 renamed raw_results to raw_protocol;
2010-08-15 wenzelm 2010-08-15 renamed create_id to new_id;
2010-08-15 wenzelm 2010-08-15 renamed class Document to Document.Version etc.; renamed Change.prev to Change.previous, and Change.document to Change.current; tuned;
2010-08-15 wenzelm 2010-08-15 fixed Isabelle/Scala build (cf. f3220ef79d51);
2010-08-14 wenzelm 2010-08-14 Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;
2010-08-14 wenzelm 2010-08-14 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
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 Document.id (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 Isabelle_Process.Result.properties;
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;