src/Pure/System/session.scala
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-12 wenzelm 2011-08-12 normalized theory dependencies wrt. file_store;
2011-08-12 wenzelm 2011-08-12 simplified class Thy_Header;
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-08-11 wenzelm 2011-08-11 explicit datatypes for document node edits;
2011-07-11 wenzelm 2011-07-11 JVM method invocation service via Scala layer;
2011-07-11 wenzelm 2011-07-11 some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;
2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-09 wenzelm 2011-07-09 echo prover input via raw_messages, for improved protocol tracing;
2011-07-09 wenzelm 2011-07-09 tuned;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-07-09 wenzelm 2011-07-09 clarified propagation of node name and header;
2011-07-09 wenzelm 2011-07-09 more precise treatment of prover definedness;
2011-07-09 wenzelm 2011-07-09 tuned source structure;
2011-07-07 wenzelm 2011-07-07 explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;
2011-07-07 wenzelm 2011-07-07 simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;
2011-07-05 wenzelm 2011-07-05 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
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-07-04 wenzelm 2011-07-04 quasi-static Isabelle_System -- reduced tendency towards "functorial style";
2011-07-04 wenzelm 2011-07-04 explicit class Counter;
2011-07-04 wenzelm 2011-07-04 pervasive Basic_Library in Scala; tuned;
2011-07-04 wenzelm 2011-07-04 some support for theory files within Isabelle/Scala session;
2011-07-03 wenzelm 2011-07-03 eliminated null;
2011-07-03 wenzelm 2011-07-03 more explicit edit_node vs. init_node; some support for master_dir and header;
2011-07-03 wenzelm 2011-07-03 tuned signature;
2011-07-02 wenzelm 2011-07-02 some support for Session.File_Store;
2011-07-02 wenzelm 2011-07-02 tuned signature;
2011-06-25 wenzelm 2011-06-25 proper tokens only if session is ready;
2011-06-23 wenzelm 2011-06-23 explicit import java.lang.System to prevent odd scope problems;
2011-06-18 wenzelm 2011-06-18 basic support for extended syntax styles: sub/superscript;
2011-01-13 wenzelm 2011-01-13 less verbosity;
2010-12-01 wenzelm 2010-12-01 more abstract/uniform handling of time, preferring seconds as Double;
2010-11-16 wenzelm 2010-11-16 post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
2010-11-13 wenzelm 2010-11-13 somewhat adhoc replacement for 'thus' and 'hence'; complete words as short as 2 characters, e.g. "Un";
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;