src/Pure/System/isabelle_process.ML
2011-07-12 wenzelm 2011-07-12 allow empty body for raw_message -- important for Invoke_Scala;
2011-07-11 wenzelm 2011-07-11 some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;
2011-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-07-05 wenzelm 2011-07-05 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05 wenzelm 2011-07-05 hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
2011-05-20 wenzelm 2011-05-20 added Isabelle_Process.is_active; tuned signature;
2010-11-13 wenzelm 2010-11-13 back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
2010-11-12 wenzelm 2010-11-12 defensive defaults for more robust experience for new users;
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-10-25 wenzelm 2010-10-25 explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt; eliminated auto_flush threads -- use plain line buffering for stdout/stderr; tuned;
2010-10-25 wenzelm 2010-10-25 more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-27 wenzelm 2010-09-27 renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
2010-09-23 wenzelm 2010-09-23 manage persistent syslog via Session, not Isabelle_Process; tuned;
2010-09-22 wenzelm 2010-09-22 more content for Session_Dockable;
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 Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
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-17 wenzelm 2010-09-17 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-17 wenzelm 2010-09-17 Isabelle_Process: status/report do not require serial numbers;
2010-09-09 wenzelm 2010-09-09 main command loops are supposed to be uninterruptible -- no special treatment here;
2010-08-30 wenzelm 2010-08-30 message serial number indicates physical order;
2010-08-16 wenzelm 2010-08-16 simplified internal message format: dropped special Symbol.STX header;
2010-08-11 wenzelm 2010-08-11 native Isabelle_Process commands, based on efficient byte channel protocol for string lists; misc clarification of proc/pid state, eliminated closing flag; misc tuning and simplification;
2010-08-10 wenzelm 2010-08-10 renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
2010-08-10 wenzelm 2010-08-10 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names; asynchronous Isabelle_Process.init -- raw ML toplevel stays active; simplified Isabelle_Process using actors; misc tuning;
2010-08-09 wenzelm 2010-08-09 auto_flush: higher frequency;
2010-08-09 wenzelm 2010-08-09 more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
2010-08-09 wenzelm 2010-08-09 Isabelle_Process: separate input fifo for commands (still using the old tty protocol); some partial workarounds for Cygwin;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-07 wenzelm 2010-08-07 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-07-03 wenzelm 2010-07-03 Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-30 wenzelm 2010-05-30 Isabelle_Process: do not enforce future_terminal_proof by default -- no error propagation yet;
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-25 wenzelm 2010-05-25 eliminated obsolete priority message from Isabelle_Process protocol;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-07 wenzelm 2010-05-07 output symbolic pretty printing markup and format in the front end;
2010-01-04 wenzelm 2010-01-04 report keywords as singleton messages, control message kind via print mode;
2009-12-30 wenzelm 2009-12-30 simplified init message -- removed redundant session property;
2009-12-29 wenzelm 2009-12-29 removed slightly odd Isar_Document.init; simplified begin_document: associate empty command/state with no_id, which is implicit start; replaced make_id by create_id (cf. Scala version); eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var; tuned;
2009-12-17 wenzelm 2009-12-17 simplified message format: chunks with explicit size in bytes; robust message header via YXML.binary_text; standard_message: refer to thread position only; discontinued obsolete "-" output stream; tuned;
2009-10-27 wenzelm 2009-10-27 non-critical output -- ship message in one piece;
2009-09-30 wenzelm 2009-09-30 actually perform Isar_Document.init on startup;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-25 wenzelm 2009-06-25 renamed IsabelleProcess to Isabelle_Process; renamed IsabelleSystem to Isabelle_System;
2009-06-02 wenzelm 2009-06-02 IsabelleProcess: emit status "ready" after initialization and reports;
2009-02-28 wenzelm 2009-02-28 moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);